powersHom — Mathlib

English

Monoid homomorphisms from Multiplicative Nat to M are in bijection with elements of M, via mapping x ↦ (Multiplicative Nat →* M) with n ↦ x^n and inverse f ↦ f(1).

Русский

Гомоморфизмы моноидов от Multiplicative Nat к M образуют биекцию с элементами M: x ↦ (n ↦ x^n) и обратное f ↦ f(1).

LaTeX

$$$ M \simeq (MonoidHom (Multiplicative Nat) M)$$$

Lean4

/-- Monoid homomorphisms from `Multiplicative ℕ` are defined by the image
of `Multiplicative.ofAdd 1`. -/
def powersHom : M ≃ (Multiplicative ℕ →* M) :=
  Additive.ofMul.trans <| (multiplesHom _).trans <| AddMonoidHom.toMultiplicativeLeft

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