English
If M is a free R-module and R satisfies StrongRankCondition, then the module rank equals the spanRank of the top submodule: rank_R(M) = (⊤).spanRank.
Русский
Если M свободный R-модуль и R удовлетворяет условию StrongRankCondition, то ранг модуля равен spanRank верхнего подмодуля: rank_R(M) = (⊤).spanRank.
LaTeX
$$$\operatorname{rank}_R(M) = (\top : Submodule R M).\operatorname{spanRank}$$$
Lean4
theorem rank_eq_spanRank_of_free [Module.Free R M] [StrongRankCondition R] :
Module.rank R M = (⊤ : Submodule R M).spanRank :=
by
haveI := nontrivial_of_invariantBasisNumber R
obtain ⟨I, B⟩ := ‹Module.Free R M›
rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]
