Commit 2025-03-14 10:49 17b56b42

refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank (#22902) Many results using Smith Normal Form for ideals of a finite free ring over a PID are also true in the case of submodules of full rank. Therefore we generalize the existing proofs to this case (usually the proofs work almost as is) and prove the corresponding results for submodules of full rank in two new files:

• LinearAlgebra.FreeModule.Finite.Quotient: we prove in particular that for M a free finite module over a PID R and a submodule N of M of same rank, we have

(M ⧸ N) ≃ₗ[R] Π i, R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R) 

• LinearAlgebra.FreeModule.Finite.CardQuotient: we prove in particular that if M is a free finite ℤ-module of basis b and N is a submodule of basis bN of the same dimension, then

(b.det ((↑) ∘ bN)).natAbs = Nat.card (M ⧸ N)

The original proofs about ideals are deduced as consequences of the generalized proofs.