charZero_ofNat — Mathlib

English

For any additive monoid with one and CharZero, the natural numbers embedded via OfNat are nonzero (in particular n ≥ 2 gives NeZero).

Русский

Для любого аддитивного моноида с единицей и CharZero отображения чисел Нат через OfNat остаются ненулевыми (в частности, n ≥ 2 даёт не нуль).

LaTeX

$$$\\mathrm{NeZero}(\\mathrm{OfNat}(n)) \\text{ for } n \\ge 2$$$

Lean4

instance charZero_ofNat {M} {n : ℕ} [n.AtLeastTwo] [AddMonoidWithOne M] [CharZero M] : NeZero (OfNat.ofNat n : M) :=
  ⟨OfNat.ofNat_ne_zero n⟩

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