Commit 2026-01-26 22:26 6fb424da

View on Github →

chore(CategoryTheory/Limits): fix name of Fan.IsLimit.desc (#34358) This is renamed as Fan.IsLimit.lift.

Estimated changes

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

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

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

deleted def CategoryTheory.Limits.Fan.IsLimit.desc

added def CategoryTheory.Limits.Fan.IsLimit.lift