instNoZeroDivisors — Mathlib

English

If α has Zero, Mul, and NoZeroDivisors, then the opposite αᵐᵒᵖ also has NoZeroDivisors, with the defining property carried over via the op map.

Русский

Если у α есть нуль, умножение и нет нулевых делителей, то и противоположный тип αᵐᵒᵖ имеет NoZeroDivisors, зафиксированное через отображение op.

LaTeX

$$MulOpposite.instNoZeroDivisors$$

Lean4

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

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