English
Additive homomorphisms ℤ →+ β are completely determined by the image of 1; the map x ↦ (n ↦ n•x) is an equivalence between β and ℤ →+ β.
Русский
Аддитивные гомоморфизмы ℤ →+ β полностью определяются по образу 1; отображение x ↦ (n ↦ n•x) задаёт эквивалентность между β и ℤ →+ β.
LaTeX
$$$$ β \\cong (\\mathbb{Z} \\to_+ β). $$$$
Lean4
/-- Additive homomorphisms from `ℤ` are defined by the image of `1`. -/
def zmultiplesHom : β ≃ (ℤ →+ β)
where
toFun
x :=
{ toFun := fun n => n • x
map_zero' := zero_zsmul x
map_add' := fun _ _ => add_zsmul _ _ _ }
invFun f := f 1
left_inv := one_zsmul
right_inv f := AddMonoidHom.ext_int <| one_zsmul (f 1)
