coe_basisOfTopLeSpanOfCardEqFinrank

English

A basis can be constructed from a top-span relation and a finrank equality.

Русский

Базис можно построить из отношений верхнего порождения и равенства финразмерности.

LaTeX

$$$\text{basisOfTopLeSpanOfCardEqFinrank}\; b \,\, \text{exists with data}$$$

Lean4

@[simp]
theorem coe_basisOfTopLeSpanOfCardEqFinrank {ι : Type*} [Fintype ι] (b : ι → V) (le_span : ⊤ ≤ span K (Set.range b))
    (card_eq : Fintype.card ι = finrank K V) : ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b :=
  Basis.coe_mk _ _

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