[Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective#39764

vlad902 wants to merge 6 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

vlad902:projective-directsumvlad902/mathlib4:projective-directsumCopy head branch name to clipboard