ofFreeGroupEquiv — Mathlib

English

Isomorphic free groups have equivalent bases (as generators).

Русский

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

LaTeX

$$$$ \\mathrm{Generators}(\\mathrm{FreeGroup}(\\alpha)) \\cong \\mathrm{Generators}(\\mathrm{FreeGroup}(\\beta)). $$$$

Lean4

/-- Isomorphic free groups have equivalent bases. -/
def ofFreeGroupEquiv (e : FreeGroup α ≃* FreeGroup β) : α ≃ β :=
  .ofFreeAbelianGroupEquiv (MulEquiv.toAdditive e.abelianizationCongr)

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