Commit 2024-03-26 11:50 d5876416

View on Github →

chore: remove duplicates of IsLimit.op and variants (#11683)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

deleted def CategoryTheory.Limits.isColimitConeOp

deleted def CategoryTheory.Limits.isColimitConeUnop

deleted def CategoryTheory.Limits.isLimitCoconeOp

deleted def CategoryTheory.Limits.isLimitCoconeUnop

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