fromMultiplicativeIntEquiv — Mathlib

English

For any group α, there is a canonical bijection between monoid homomorphisms from the multiplicative integers to α and elements of α; the inverse is given by zpowersHom.

Русский

Для любой группы α существует каноническое биекцию между MonoidHom (Multiplicative ℤ) α и элементами α; обратная связка задаётся через zpowersHom.

LaTeX

$$$$ (\mathrm{Multiplicative} \mathbb{Z} \to* \alpha) \cong \alpha $$$$

Lean4

/-- The equivalence `(Multiplicative ℤ →* α) ≃ α` for any group `α`. -/
@[deprecated zpowersHom (since := "2025-05-11")]
def fromMultiplicativeIntEquiv (α : Type u) [Group α] : (Multiplicative ℤ →* α) ≃ α :=
  (zpowersHom _).symm

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