Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-20 23:38 99ba8f44

View on Github →

chore(category_theory): change monoidal_of_has_finite_products to use binary products (#2190)

chore(category_theory): change monoidal_of_has_finite_products to use binary products
remove some simp annotations for now
fixes

Estimated changes

Modified src/category_theory/monoidal/of_has_finite_products.lean

added theorem category_theory.monoidal_of_has_finite_coproducts.associator_hom

added theorem category_theory.monoidal_of_has_finite_coproducts.left_unitor_hom

added theorem category_theory.monoidal_of_has_finite_coproducts.left_unitor_inv

added theorem category_theory.monoidal_of_has_finite_coproducts.right_unitor_hom

added theorem category_theory.monoidal_of_has_finite_coproducts.right_unitor_inv

modified def category_theory.monoidal_of_has_finite_coproducts

added theorem category_theory.monoidal_of_has_finite_products.associator_hom

added theorem category_theory.monoidal_of_has_finite_products.left_unitor_hom

added theorem category_theory.monoidal_of_has_finite_products.left_unitor_inv

added theorem category_theory.monoidal_of_has_finite_products.right_unitor_hom

added theorem category_theory.monoidal_of_has_finite_products.right_unitor_inv

modified def category_theory.monoidal_of_has_finite_products