Commit 2022-11-14 20:05 b8e1f0f7

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.