basisOfTopLeSpanOfCardEqFinrank — Mathlib

English

The coe of the basis constructed from top-span data equals the original vector family.

Русский

Коэффициент-образ базиса, построенного из данных о порождении сверху, равен исходному семейству вектора.

LaTeX

$$$\mathrm{coe}(\mathrm{basisOfTopLeSpanOfCardEqFinrank}\; b\; \ldots) = b$$$

Lean4

/-- A family of `finrank K V` vectors forms a basis if they span the whole space. -/
noncomputable def basisOfTopLeSpanOfCardEqFinrank {ι : Type*} [Fintype ι] (b : ι → V)
    (le_span : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) : Basis ι K V :=
  Basis.mk (linearIndependent_of_top_le_span_of_card_eq_finrank le_span card_eq) le_span

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