instNoZeroDivisors — Mathlib

English

Opposite of a NoZeroDivisors ring inherits NoZeroDivisors: if op(x)·op(y) = op(0), then x = 0 or y = 0.

Русский

Прямопреобразование противоположного кольца сохраняет свойство отсутствия нулевых делителей: если op(x)·op(y) = op(0), то x=0 или y=0.

LaTeX

$$$\forall x,y,\ op(x)\cdot op(y) = op(0) \Rightarrow x=0 \lor y=0$$$

Lean4

instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ where
  eq_zero_or_eq_zero_of_mul_eq_zero
    (H :
      op (_ * _) =
        op
          (0 :
            α)) :=
    Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
      (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)

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