Def SSet.Subcomplex.unionProd.ιIso

Modification history

2026-04-27 21:20

Mathlib/AlgebraicTopology/SimplicialSet/PushoutProduct.lean

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

Added SSet.Subcomplex.unionProd.ιIso View on Github →