mathlib3

666d8787 - feat(algebra/module/projective): projective modules are closed under direct sums (#16743)

feat(algebra/module/projective): projective modules are closed under direct sums (#16743) I'm unsure what the universe should be for the index type `ι` in algebra/module/projective (`{ι : Type*}` doesn't work). - [x] depends on: #16735 Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>