instNoNatZeroDivisorsOfIsAddTorsionFree

English

If M is an AddCommMonoid and IsAddTorsionFree, then M has no natural-number zero divisors; i.e., na = 0 with n ≠ 0 implies a = 0.

Русский

Пусть M — коммутативный аддитивный моноид и IsAddTorsionFree. Тогда в M нет натуральных нулевых делителей: если n⋅a = 0 и n ≠ 0, то a = 0.

LaTeX

$$[AddCommMonoid M] [IsAddTorsionFree M] ⇒ NoNatZeroDivisors M$$

Lean4

instance [AddCommMonoid M] [IsAddTorsionFree M] : Lean.Grind.NoNatZeroDivisors M where
  no_nat_zero_divisors _ _ _ hk habk := IsAddTorsionFree.nsmul_right_injective hk habk

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