chooseBasis — Mathlib

English

If M is free, then chooseBasis R M is a basis of M with index type ChooseBasisIndex R M.

Русский

Если M свободен, то chooseBasis R M является базисом M с индексным множеством ChooseBasisIndex R M.

LaTeX

$$$$ \mathrm{chooseBasis} : \mathrm{Basis}(\mathrm{ChooseBasisIndex}(R,M),R,M) $$$$

Lean4

/-- If `Module.Free R M` then `chooseBasis : ι → M` is the basis.
Here `ι = ChooseBasisIndex R M`. -/
noncomputable def chooseBasis : Basis (ChooseBasisIndex R M) R M :=
  ((Module.free_iff_set R M).mp ‹_›).choose_spec.some

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