rank_le_spanRank — Mathlib

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

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