Def CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct

Modification history

2023-03-07 09:14

Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

feat: port CategoryTheory.Limits.Shapes.DisjointCoproduct (#2689)

Added CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct View on Github →