mathlib

b8e1f0f7 - feat(linear_algebra/free_module): lemmas on ideal quotient of a free module over a PID (#17103)

feat(linear_algebra/free_module): lemmas on ideal quotient of a free module over a PID (#17103) This PR shows we can write the quotient by an ideal of `S` which is a finite free extension over a PID `R`, as a product of quotients of `R` by principal ideals. As a useful corollary, nonzero quotients of a finite `ℤ`-module are finite types. This is very useful in the context of ideal norms.