Commit 2025-03-01 17:18 7f8db821

View on Github →

feat: *CatMax abbrevs no longer necessary (#22417)

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Abelian.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Colimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

modified def ModuleCat.FilteredColimits.colimit

Modified Mathlib/Algebra/Category/ModuleCat/Products.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

modified def SemiRingCat.FilteredColimits.colimit

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

modified def localCohomology.ofDiagram

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean