Commit 2026-05-26 16:16 6ed0026d

View on Github →

chore(CategoryTheory/Limits): fix name of HasColimit.isoOfEquivalence_hom_π and reassoc (#39817)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π

deleted theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π

added theorem CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom

added theorem CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean