English
If α ≃ β, then FreeAbelianGroup α ≃+ FreeAbelianGroup β; isomorphism is induced by map f on generators.
Русский
Если α эквивалентен β, то свободная абелеева группа на α эквивалентна свободной абелевой группе на β; изоморфизм индуцируется отображением на генераторах.
LaTeX
$$$ \\text{For any } f: \\alpha \\simeq \\beta, \\ \\mathrm{FreeAbelianGroup}(\\alpha) \\cong_{+} \\mathrm{FreeAbelianGroup}(\\beta). $$$$
Lean4
/-- Isomorphic types have isomorphic free abelian groups. -/
def equivOfEquiv {α β : Type*} (f : α ≃ β) : FreeAbelianGroup α ≃+ FreeAbelianGroup β
where
toFun := map f
invFun := map f.symm
left_inv x := by rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]
right_inv x := by rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]
map_add' := AddMonoidHom.map_add _
