to_noZeroDivisors — Mathlib

English

Let α be a type with multiplication and a zero, and assume α is a subsingleton. Then α has no zero divisors: if x·y = 0 then x = 0 or y = 0.

Русский

Пусть α — множество с умножением и нулём, обладающее единым элементом. Тогда в α нет нулевых делителей: если x·y = 0, то x = 0 или y = 0.

LaTeX

$$$$\\forall x,y \\in \\alpha,\\ x y = 0 \\Rightarrow x=0 \\lor y=0.$$$$

Lean4

theorem to_noZeroDivisors [Mul α] [Zero α] [Subsingleton α] : NoZeroDivisors α where
  eq_zero_or_eq_zero_of_mul_eq_zero _ := .inl (Subsingleton.eq_zero _)

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