finBasis — Mathlib

English

A finite rank free module has a basis indexed by Fin(finrank R M).

Русский

Свободный модуль конечного ранга имеет базис, индексированный по Fin(finrank R M).

LaTeX

$$$$ \\text{Basis}(\\mathrm{Fin}(\\mathrm{finrank}\\,R\\,M))\\;R\\;M $$$$

Lean4

/-- A finite rank free module has a basis indexed by `Fin (finrank R M)`. -/
noncomputable def finBasis [Module.Finite R M] : Basis (Fin (finrank R M)) R M :=
  (Module.Free.chooseBasis R M).reindex (Fintype.equivFinOfCardEq (finrank_eq_card_chooseBasisIndex R M).symm)

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