Theorem CategoryTheory.Limits.map_braiding_hom_comp_prodComparison

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.map_braiding_hom_comp_prodComparisonView on Github →
2026-08-19 11:50
Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
feat(AlgebraicTopology/SimplicialSet): induction principle for morphisms of the homotopy category of a simplicial set (#42673)
Added CategoryTheory.Limits.map_braiding_hom_comp_prodComparisonView on Github →