toNoZeroDivisors — Mathlib

English

In a normed ring with a multiplicative norm, zero divisors do not exist: if ab = 0 then a = 0 or b = 0.

Русский

В нормированном кольце с мультипликативной нормой нулевых делителей нет: если ab = 0, то a = 0 или b = 0.

LaTeX

$$$ab=0\\Rightarrow a=0 \\lor b=0$$$

Lean4

instance toNoZeroDivisors : NoZeroDivisors α where
  eq_zero_or_eq_zero_of_mul_eq_zero h := by simpa only [← norm_eq_zero (E := α), norm_mul, mul_eq_zero] using h

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