zpowersHom — Mathlib

English

There is a canonical equivalence α ≃ (Multiplicative ℤ →* α) sending x ∈ α to the monoid hom n ↦ x^n.

Русский

Существует каноническое эквивалентное отображение α ≃ (Multiplicative ℤ →* α), отправляющее x ∈ α в моноид-гомоморфизм n ↦ x^n.

LaTeX

$$$$ \\alpha \\simeq (\\text{MonoidHom} (\\text{Multiplicative } \\mathbb{Z}, \\alpha)). $$$$

Lean4

/-- Monoid homomorphisms from `Multiplicative ℤ` are defined by the image
of `Multiplicative.ofAdd 1`. -/
def zpowersHom : α ≃ (Multiplicative ℤ →* α) :=
  ofMul.trans <| (zmultiplesHom _).trans <| AddMonoidHom.toMultiplicativeLeft

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