Skip to content

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

Closed
vlad902 wants to merge 6 commits into
leanprover-community:masterfrom
vlad902:projective-directsum
Closed

[Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective#39764
vlad902 wants to merge 6 commits into
leanprover-community:masterfrom
vlad902:projective-directsum

delete unnecessary import

ae42657
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded May 24, 2026 in 1m 23s