feat: add Module.finrank_quotient_add_finrank_le (#17782)

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Module.Torsion
 import Mathlib.SetTheory.Cardinal.Cofinality
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
+import Mathlib.LinearAlgebra.Dimension.Constructions
 
 /-!
 # Conditions for rank to be finite
@@ -426,6 +427,14 @@ theorem Module.finrank_zero_iff [NoZeroSMulDivisors R M] :
   rw [← rank_zero_iff (R := R), ← finrank_eq_rank]
   norm_cast
 
+/-- Similar to `rank_quotient_add_rank_le` but for `finrank` and a finite `M`. -/
+lemma Module.finrank_quotient_add_finrank_le (N : Submodule R M) :
+    finrank R (M ⧸ N) + finrank R N ≤ finrank R M := by
+  haveI := nontrivial_of_invariantBasisNumber R
+  have := rank_quotient_add_rank_le N
+  rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this
+  exact mod_cast this
+
 end StrongRankCondition
 
 theorem Module.finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) :

Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

@@ -443,6 +443,13 @@ noncomputable instance {R M : Type*} [DivisionRing R] [AddCommGroup M] [Module R
 theorem finrank_eq_rank [Module.Finite R M] : ↑(finrank R M) = Module.rank R M := by
   rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]
 
+/-- If `M` is finite, then `finrank N = rank N` for all `N : Submodule M`. Note that
+such an `N` need not be finitely generated. -/
+protected theorem _root_.Submodule.finrank_eq_rank [Module.Finite R M] (N : Submodule R M) :
+    finrank R N = Module.rank R N := by
+  rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]
+  exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)
+
 end Module
 
 open Module