pith. machine review for the scientific record. sign in
theorem proved tactic proof

mul_eq_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 408theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by

proof body

Tactic-mode proof.

 409  constructor
 410  · intro h
 411    have hint : toInt a * toInt b = 0 := by
 412      rw [← toInt_mul]
 413      have := congrArg toInt h
 414      rwa [toInt_zero] at this
 415    rcases Int.mul_eq_zero.mp hint with ha | hb
 416    · left
 417      rw [eq_iff_toInt_eq, toInt_zero]; exact ha
 418    · right
 419      rw [eq_iff_toInt_eq, toInt_zero]; exact hb
 420  · rintro (ha | hb)
 421    · rw [ha, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 422    · rw [hb, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 423
 424/-- Cancellation: if `c ≠ 0` and `a * c = b * c`, then `a = b`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.