Isomorphisms between free groups imply equivalences of their generators

noncomputable def FreeAbelianGroup.basis (α : Type u_5) : Module.Basis α ℤ (FreeAbelianGroup α)

A is a basis of the ℤ-module FreeAbelianGroup A.

noncomputable def Equiv.ofFreeAbelianGroupLinearEquiv {α : Type u_1} {β : Type u_2} (e : FreeAbelianGroup α ≃ₗ[ℤ] FreeAbelianGroup β) : α ≃ β

Isomorphic free abelian groups (as modules) have equivalent bases.

noncomputable def Equiv.ofFreeAbelianGroupEquiv {α : Type u_1} {β : Type u_2} (e : FreeAbelianGroup α ≃+ FreeAbelianGroup β) : α ≃ β

Isomorphic free abelian groups (as additive groups) have equivalent bases.

noncomputable def Equiv.ofFreeGroupEquiv {α : Type u_1} {β : Type u_2} (e : FreeGroup α ≃* FreeGroup β) : α ≃ β

Isomorphic free groups have equivalent bases.

noncomputable def Equiv.ofIsFreeGroupEquiv {G : Type u_3} {H : Type u_4} [Group G] [Group H] [IsFreeGroup G] [IsFreeGroup H] (e : G ≃* H) : IsFreeGroup.Generators G ≃ IsFreeGroup.Generators H

Isomorphic free groups have equivalent bases (IsFreeGroup variant).