fromMultiplicativeNatEquiv — Mathlib

English

There is a canonical equivalence between Monoid homs from Multiplicative Nat to a monoid α and α itself; i.e., (Multiplicative ℕ →* α) ≃ α.

Русский

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

LaTeX

$$$(\mathrm{Multiplicative}\ \mathbb{N} \to^* \alpha) \simeq \alpha$$$

Lean4

/-- The equivalence `(Multiplicative ℕ →* α) ≃ α` for any monoid `α`. -/
@[deprecated powersHom (since := "2025-05-11")]
def fromMultiplicativeNatEquiv (α : Type u) [Monoid α] : (Multiplicative ℕ →* α) ≃ α :=
  (powersHom _).symm

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