Commit 2023-03-07 09:14 7003654e

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

added theorem CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts

added def CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct