instNoZeroDivisors — Mathlib

English

SetSemiring α has no zero divisors: if a * b = 0 then a = 0 or b = 0 (provided α is a monoid).

Русский

SetSemiring α не имеет нулевых делителей: если a * b = 0, то a = 0 или b = 0 (при условии, что α — моноид).

LaTeX

$$NoZeroDivisors (SetSemiring α)$$

Lean4

instance : NoZeroDivisors (SetSemiring α) :=
  ⟨fun {a b} ab =>
    a.eq_empty_or_nonempty.imp_right fun ha =>
      b.eq_empty_or_nonempty.resolve_right fun hb => Nonempty.ne_empty ⟨_, mul_mem_mul ha.some_mem hb.some_mem⟩ ab⟩

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