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