chore: forward-port leanprover-community/mathlib#19084 (file 2 of 2) (#…

…4821)

[`linear_algebra.free_module.ideal_quotient`@`6623e6af705e97002a9054c1c05a980180276fc1`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/ideal_quotient?range=6623e6af705e97002a9054c1c05a980180276fc1..d87199d51218d36a0a42c66c82d147b5a7ff87b3)

Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

@@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 
 ! This file was ported from Lean 3 source module linear_algebra.free_module.ideal_quotient
-! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
+! leanprover-community/mathlib commit d87199d51218d36a0a42c66c82d147b5a7ff87b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.ZMod.Quotient
-import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
 import Mathlib.LinearAlgebra.FreeModule.PID
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.QuotientPi
 
 /-! # Ideals in free modules over PIDs
@@ -23,7 +24,7 @@ import Mathlib.LinearAlgebra.QuotientPi
 -/
 
 
-open BigOperators
+open scoped BigOperators DirectSum
 
 variable {ι R S : Type _} [CommRing R] [CommRing S] [Algebra R S]
 
@@ -107,3 +108,25 @@ noncomputable def Ideal.fintypeQuotientOfFreeOfNeBot [Module.Free ℤ S] [Module
     ⟨Int.natAbs_ne_zero.mpr (Ideal.smithCoeffs_ne_zero b I hI i)⟩
   classical exact Fintype.ofEquiv (∀ i, ZMod (a i).natAbs) e.symm
 #align ideal.fintype_quotient_of_free_of_ne_bot Ideal.fintypeQuotientOfFreeOfNeBot
+
+variable (F : Type _) [CommRing F] [Algebra F R] [Algebra F S] [IsScalarTower F R S]
+  (b : Basis ι R S) {I : Ideal S} (hI : I ≠ ⊥)
+
+/-- Decompose `S⧸I` as a direct sum of cyclic `R`-modules
+  (quotients by the ideals generated by Smith coefficients of `I`). -/
+noncomputable def Ideal.quotientEquivDirectSum :
+    (S ⧸ I) ≃ₗ[F] ⨁ i, R ⧸ Ideal.span ({I.smithCoeffs b hI i} : Set R) :=
+  -- porting note: manual construction of `CompatibleSmul` typeclass no longer needed
+  ((I.quotientEquivPiSpan b _).restrictScalars F).trans
+    (DirectSum.linearEquivFunOnFintype _ _ _).symm
+#align ideal.quotient_equiv_direct_sum Ideal.quotientEquivDirectSum
+
+theorem Ideal.finrank_quotient_eq_sum [Nontrivial F]
+    [∀ i, Module.Free F (R ⧸ Ideal.span ({I.smithCoeffs b hI i} : Set R))]
+    [∀ i, Module.Finite F (R ⧸ Ideal.span ({I.smithCoeffs b hI i} : Set R))] :
+    FiniteDimensional.finrank F (S ⧸ I) =
+      ∑ i, FiniteDimensional.finrank F (R ⧸ Ideal.span ({I.smithCoeffs b hI i} : Set R)) := by
+  -- slow, and dot notation doesn't work
+  rw [LinearEquiv.finrank_eq <| Ideal.quotientEquivDirectSum F b hI,
+    FiniteDimensional.finrank_directSum]
+#align ideal.finrank_quotient_eq_sum Ideal.finrank_quotient_eq_sum