Commit 2021-03-08 19:42 0afdaab2

feat(linear_algebra): submodules of f.g. free modules are free (#6178) This PR proves the first half of the structure theorem for modules over a PID: if R is a principal ideal domain and M an R-module which is free and finitely generated (expressed by is_basis R (b : ι → M), for a [fintype ι]), then all submodules of M are also free and finitely generated. This result requires some lemmas about the rank of (free) modules (which in that case is basically the same as fintype.card ι). If M were a vector space, this could just be expressed as findim R M, but it isn't necessarily, so it can't be.