Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-29 09:22 6030ff0a

View on Github →

chore(category_theory): speed-up monoidal.of_has_finite_products (#1616)

Estimated changes

Modified src/category_theory/limits/shapes/binary_products.lean

added theorem category_theory.limits.coprod.associator_naturality

added theorem category_theory.limits.coprod.pentagon

added theorem category_theory.limits.coprod.triangle

added theorem category_theory.limits.prod.associator_naturality

added theorem category_theory.limits.prod.pentagon

added theorem category_theory.limits.prod.triangle

Modified src/category_theory/monoidal/of_has_finite_products.lean