[Merged by Bors] - feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective#37449
Closed
dagurtomas wants to merge 12 commits intoleanprover-community:masterfrom
Closed
Commits
Commits on Mar 31, 2026
- committed
- committed
- authored andcommitted
- committed
Commits on Apr 7, 2026
Commits on Apr 13, 2026
Commits on Apr 18, 2026
- committed
Merge branch 'master' of github.com:leanprover-community/mathlib4 into n-infty-internally-projective
committed- authored andcommitted
- committed
- committed
