Commit 2026-10-10 17:11 81d17696

View on Github →

chore(CategoryTheory/Limits): use to_dual where we couldn't before (#44649) This PR uses to_dual in a few places that weren't possible before #44266.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted def CategoryTheory.Limits.colimit.homIso'

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

deleted def CategoryTheory.Limits.IsColimit.homIso'

deleted theorem CategoryTheory.Limits.IsColimit.homIso_hom

deleted def CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism