Def CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv

Modification history

2026-08-20 12:19

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

refactor(CategoryTheory/Limits/Shapes): split up BinaryProducts.lean (#42917) …

Modified CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv View on Github →

2026-05-23 12:42

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

chore(CategoryTheory/Limits): some API for binary (co)products (#39594) …

Added CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv View on Github →