mul_eq_zero — Mathlib

English

In a NoZeroDivisors setting, a·b = 0 iff a = 0 or b = 0.

Русский

В условиях NoZeroDivisors, a·b = 0 тогда и только тогда, когда a = 0 или b = 0.

LaTeX

$$$\operatorname{NoZeroDivisors}(M_0) \Rightarrow (a\cdot b = 0 \iff a=0 \lor b=0)$$$

Lean4

/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
equals zero. -/
@[simp]
theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=
  ⟨eq_zero_or_eq_zero_of_mul_eq_zero, fun o ↦ o.elim (fun h ↦ mul_eq_zero_of_left h b) (mul_eq_zero_of_right a)⟩

Похожие утверждения