Step
*
of Lemma
mul_ident
∀[i:ℤ]. (i = (i * 1) ∈ ℤ)
BY
{ Auto }
Latex:
Latex:
\mforall{}[i:\mBbbZ{}].  (i  =  (i  *  1))
By
Latex:
Auto
Home
Index