setBasisOfTopLeSpanOfCardEqFinrank

English

The top subalgebra and its top submodule have the same rank.

Русский

У верхней подалгебры и верхнего подмодуля совпадает ранг.

LaTeX

$$$\operatorname{Module.rank}_F(\top_{\text{Subalgebra}}) = \operatorname{Module.rank}_F(\top_{\text{Submodule}})$$$

Lean4

/-- A set of `finrank K V` vectors forms a basis if they span the whole space. -/
@[simps! repr_apply]
noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {s : Set V} [Fintype s] (le_span : ⊤ ≤ span K s)
    (card_eq : s.toFinset.card = finrank K V) : Basis s K V :=
  basisOfTopLeSpanOfCardEqFinrank ((↑) : s → V) ((@Subtype.range_coe_subtype _ s).symm ▸ le_span)
    (_root_.trans s.toFinset_card.symm card_eq)

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