ChooseBasisIndex — Mathlib

English

If Module.Free R M holds, then the index type ChooseBasisIndex R M indexes a basis for M.

Русский

Если Module.Free R M выполняется, то тип ChooseBasisIndex R M индексирует базис для M.

LaTeX

$$$$ \text{ChooseBasisIndex }R M := \text{the index type of a basis for } M $$$$

Lean4

/-- If `Module.Free R M` then `ChooseBasisIndex R M` is the `ι` which indexes the basis
  `ι → M`. Note that this is defined such that this type is finite if `R` is trivial. -/
def ChooseBasisIndex : Type _ :=
  ((Module.free_iff_set R M).mp ‹_›).choose

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