Commit 2024-03-17 01:49 7acbfc58

View on Github →

feat: preserves colimit if colimit.post is iso (#11421)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Limits.lean

added def CategoryTheory.preservesColimitOfIsIsoPost

added def CategoryTheory.preservesLimitOfIsIsoPost