fromIntEquiv — Mathlib

English

For any additive group α, there is a canonical bijection between AddMonoidHom Int α and α; the inverse is given by zmultiplesHom.

Русский

Для любой аддитивной группы α существует каноническая биекция между AddMonoidHom Int α и α; обратная связь задаётся через zmultiplesHom.

LaTeX

$$$$ (\mathbb{Z} \to+ α) \simeq α $$$$

Lean4

/-- The equivalence `(ℤ →+ α) ≃ α` for any additive group `α`. -/
@[deprecated zmultiplesHom (since := "2025-05-11")]
def fromIntEquiv (α : Type u) [AddGroup α] : (ℤ →+ α) ≃ α :=
  (zmultiplesHom _).symm

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