Theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'

Modification history

2026-06-25 07:54

Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean

chore: remove unused instances (#41013) …

Modified CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'View on Github →

2026-04-27 21:20

Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean

feat(CategoryTheory/Monoidal/PushoutProduct): isomorphisms and lifting properties of pushout-products (#37198) …

Added CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'View on Github →