Theorem CategoryTheory.Limits.prodComparison_natural_of_natTrans

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.prodComparison_natural_of_natTransView on Github →
2025-10-28 23:08
Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added CategoryTheory.Limits.prodComparison_natural_of_natTransView on Github →