Step
*
1
1
of Lemma
zero_divs_only_zero
1. a : ℤ
2. c : ℤ
3. a = (0 * c) ∈ ℤ
⊢ a = 0 ∈ ℤ
BY
{ TACTIC:Auto }
Latex:
Latex:
1.  a  :  \mBbbZ{}
2.  c  :  \mBbbZ{}
3.  a  =  (0  *  c)
\mvdash{}  a  =  0
By
Latex:
TACTIC:Auto
Home
Index