English
If α is a commutative group, there is a multiplicative equivalence between α and the monoid homomorphisms from Multiplicative ℤ to α, given by a ↦ (n ↦ a^n) with inverse f ↦ f(1).
Русский
Пусть α — коммутативная группа. Существует мультипликативная эквивалентность α≃* MonoidHom(Multiplicative ℤ, α), заданная через a↦(n↦a^n) и обратное f↦f(1).
LaTeX
$$$\\zpowersMulHom:\\ α \\simeq_* (MonoidHom (Multiplicative \\mathbb{Z})\\; \\alpha)$, где $(\\zpowersMulHom\\; a)(n)=a^n$ и $(\\zpowersMulHom)^{-1}(f)=f(1)$$$
Lean4
/-- If `α` is commutative, `zpowersHom` is a multiplicative equivalence. -/
def zpowersMulHom : α ≃* (Multiplicative ℤ →* α) :=
{ zpowersHom α with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_zpow] }
