ofIsFreeGroupEquiv — Mathlib

English

Isomorphic free groups have equivalent bases (IsFreeGroup variant).

Русский

Изоморфные свободные группы имеют эквивалентные базы (вариант IsFreeGroup).

LaTeX

$$$$ \\text{Equiv}_{IsFreeGroup}(G,H): \\mathrm{Generators}(G) \\cong \\mathrm{Generators}(H). $$$$

Lean4

/-- Isomorphic free groups have equivalent bases (`IsFreeGroup` variant). -/
def ofIsFreeGroupEquiv [Group G] [Group H] [IsFreeGroup G] [IsFreeGroup H] (e : G ≃* H) : Generators G ≃ Generators H :=
  .ofFreeGroupEquiv <| (toFreeGroup G).symm.trans <| e.trans <| toFreeGroup H

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