infinite — Mathlib

English

In a CharZero additive monoid M, the map ℕ → M given by n ↦ n is injective; hence M is infinite.

Русский

В аддитивном моноиде M с CharZero отображение $\\mathbb{N} \\to M$, $n \\mapsto n$, инъективно; следовательно M бесконечен.

LaTeX

$$$ \\forall n,m \\in \\mathbb{N},\\ n \\neq m \\Rightarrow n \\cdot 1_M \\neq m \\cdot 1_M $$$

Lean4

instance (priority := 100) infinite : Infinite M :=
  Infinite.of_injective Nat.cast Nat.cast_injective

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