instNoZeroDivisors — Mathlib

English

If a and b are Nimbers and a*b = 0, then either a = 0 or b = 0.

Русский

Если a и b — Nimber и a*b = 0, то либо a = 0, либо b = 0.

LaTeX

$$$ a \cdot b = 0 \Rightarrow (a = 0) \lor (b = 0)$$$

Lean4

instance : NoZeroDivisors Nimber where
  eq_zero_or_eq_zero_of_mul_eq_zero {a b}
    h := by
    by_contra! hab
    iterate 2 rw [← Nimber.pos_iff_ne_zero] at hab
    apply (mul_ne_of_lt _ hab.1 _ hab.2).symm
    simpa only [zero_add, mul_zero, zero_mul]

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