ofFreeAbelianGroupEquiv — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\text{basis}_{\\mathrm{FreeAbelianGroup}}(\\alpha) \\cong \\text{basis}_{\\mathrm{FreeAbelianGroup}}(\\beta) $$$$

Lean4

/-- Isomorphic free abelian groups (as additive groups) have equivalent bases. -/
def ofFreeAbelianGroupEquiv (e : FreeAbelianGroup α ≃+ FreeAbelianGroup β) : α ≃ β :=
  .ofFreeAbelianGroupLinearEquiv e.toIntLinearEquiv

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