English
If M' ≤ torsion R M, then the rank of the quotient M/M' equals the rank of M.
Русский
Если M' ≤ torsion R M, то ранг модуля M/M' равен рангу M.
LaTeX
$$$\\operatorname{Module.rank} R (M / M') = \\operatorname{Module.rank} R M$$$
Lean4
theorem rank_quotient_eq_of_le_torsion {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {M' : Submodule R M}
(hN : M' ≤ torsion R M) : Module.rank R (M ⧸ M') = Module.rank R M :=
(rank_quotient_le M').antisymm <| by
nontriviality R
rw [Module.rank]
refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_
rw [LinearIndepOn, linearIndependent_iff'] at hs
simp_rw [linearIndependent_iff', ← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]
intro t g hg i hi
obtain ⟨r, hg⟩ := hN hg
simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg
exact r.prop.2 _ (mul_comm (g i) r ▸ hs t _ hg i hi)
