English
Assuming StrongRankCondition on R, Module.rank_R(M) ≤ (⊤ : Submodule R M).spanRank.
Русский
При условии StrongRankCondition для кольца R выполняется: rank_R(M) ≤ (⊤).spanRank.
LaTeX
$$$\operatorname{rank}_R(M) \le (\top : Submodule R M).\operatorname{spanRank}$$$
Lean4
theorem rank_le_spanRank [StrongRankCondition R] : Module.rank R M ≤ (⊤ : Submodule R M).spanRank :=
by
rw [Module.rank, Submodule.spanRank]
refine ciSup_le' (fun ι ↦ (le_ciInf fun s ↦ ?_))
have := linearIndependent_le_span'' ι.2 s.1 s.2
simpa