noZeroDivisors — Mathlib

English

NoZeroDivisors holds in GroupWithZero: if a · b = 0, then a = 0 or b = 0.

Русский

У группы с нулём выполняется отсутствие нулевых делителей: если a·b = 0, то a = 0 или b = 0.

LaTeX

$$$a,b \in G_0 \Rightarrow (a\cdot b = 0 \Rightarrow a = 0 \lor b = 0)$$$

Lean4

instance (priority := 10) noZeroDivisors : NoZeroDivisors G₀ :=
  { (‹_› : GroupWithZero G₀) with
    eq_zero_or_eq_zero_of_mul_eq_zero :=
      @fun a b h => by
        contrapose! h
        exact (Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero }
    -- Can't be put next to the other `mk0` lemmas because it depends on the
    -- `NoZeroDivisors` instance, which depends on `mk0`.

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