mk_eq_spanRank — Mathlib

English

For a basis v of M over R, the cardinality of its range equals the spanRank of the top submodule, i.e., the rank of M equals the spanRank of M.

Русский

Для базиса v модуля M над R кардинал множества его элементов равен spanRank верхнего подмодуля, то есть рангу M.

LaTeX

$$$\#\mathrm{Set.range}(v) = (\top : Submodule R M).\spanRank$$$

Lean4

theorem mk_eq_spanRank [RankCondition R] {ι : Type*} (v : Basis ι R M) :
    #(Set.range v) = (⊤ : Submodule R M).spanRank :=
  by
  rw [← v.span_eq, spanRank_span_of_linearIndepOn]
  exact v.linearIndependent.linearIndepOn_id

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