charZero — Mathlib

English

If M is a CharZero additive monoid with one, then M is infinite; equivalently, the natural map n ↦ n · 1 is injective.

Русский

Если M — аддитивный моноид с единицей и характеристика ноль, то M бесконечен; эквивалентно инъективности отображения натуралов в M, n ↦ n·1.

LaTeX

$$$ \operatorname{Infinite}(M) \quad\text{or equivalently} \quad\forall n,m \in \mathbb{N},\ n \neq m \Rightarrow n\cdot 1_M \neq m\cdot 1_M $$$

Lean4

instance charZero {M} {n : ℕ} [NeZero n] [AddMonoidWithOne M] [CharZero M] : NeZero (n : M) :=
  ⟨Nat.cast_ne_zero.mpr out⟩

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