ofNatHom — Mathlib

English

There exists a canonical ring homomorphism from the natural numbers into the integers, sending each n to its standard integer value.

Русский

Существует канонический гомоморфизм колец от натуральных чисел к целым, отправляющий каждое n в соответствующее целое число.

LaTeX

$$$ \exists f: \mathbb{N} \to^+ \mathbb{Z}, \forall n \in \mathbb{N}, f(n) = n.$$$

Lean4

/-- Coercion `ℕ → ℤ` as a `RingHom`. -/
def ofNatHom : ℕ →+* ℤ :=
  Nat.castRingHom ℤ

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