fromNatEquiv — Mathlib

English

There is a canonical equivalence between AddMonoid homs from Nat to an additive monoid α and α itself; i.e., (ℕ →+ α) ≃ α.

Русский

Существует каноническое эквивалентное отображение между гомоморфизмами AddMonoid из ℕ в аддитивный моноид α и самим α; то есть (ℕ →+ α) ≃ α.

LaTeX

$$$(\mathrm{Nat} \to^+ \alpha) \simeq \alpha$$$

Lean4

/-- The equivalence `(ℕ →+ α) ≃ α` for any additive monoid `α`. -/
@[deprecated multiplesHom (since := "2025-05-11")]
def fromNatEquiv (α : Type u) [AddMonoid α] : (ℕ →+ α) ≃ α :=
  (multiplesHom _).symm

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