Commit 2026-05-20 12:46 06f1f222

View on Github →

chore(CategoryTheory/Limits): rename mkFanLimit to Fan.IsLimit.mk (#39580) This change makes Fan follow the ConeType.IsLimit.mk naming scheme that we use elsewhere. We do the same for Cofans.

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/GradedObject/Unitor.lean

Modified Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean

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

Modified Mathlib/CategoryTheory/Limits/FormalCoproducts/Cech.lean

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

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

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

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

added def CategoryTheory.Limits.Cofan.IsColimit.mk

added def CategoryTheory.Limits.Fan.IsLimit.mk

deleted def CategoryTheory.Limits.mkCofanColimit

deleted def CategoryTheory.Limits.mkFanLimit

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean