ofFreeAbelianGroupLinearEquiv — Mathlib

English

Transport a FreeGroupBasis along a group isomorphism e: G ≃* H to obtain a FreeGroupBasis on H, defined by composing the representation with e.

Русский

Перенос базиса свободной группы по изоморфизму группы e: G ≃* H даёт базис на H, определяемый композиция представления с e.

LaTeX

$$$$ \\text{map}(b,e) : \\mathrm{FreeGroupBasis}(\\text{on }H) \\text{ with } (\\text{map}(b,e)).repr = e^{-1} \\circ b.repr. $$$$

Lean4

/-- Isomorphic free abelian groups (as modules) have equivalent bases. -/
def ofFreeAbelianGroupLinearEquiv (e : FreeAbelianGroup α ≃ₗ[ℤ] FreeAbelianGroup β) : α ≃ β :=
  let t : Basis α ℤ (FreeAbelianGroup β) := (FreeAbelianGroup.basis α).map e
  t.indexEquiv <| FreeAbelianGroup.basis _

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