zero_eq_mul — Mathlib

English

If NoZeroDivisors holds, then 0 = a·b iff a = 0 or b = 0.

Русский

Если выполняется NoZeroDivisors, то 0 = a·b эквивалентно a = 0 или b = 0.

LaTeX

$$$\text{NoZeroDivisors}(M_0) \Rightarrow (0 = a \cdot b \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 zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0 := by rw [eq_comm, mul_eq_zero]

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