Commit 2023-06-08 16:01 d6a4e2fe

View on Github →

feat: port CategoryTheory.Monoidal.OfHasFiniteProducts (#4826)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj

added def CategoryTheory.monoidalOfHasFiniteCoproducts

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom

added theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_hom

added theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_inv

added theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_hom

added theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_inv

added theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorHom

added theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorObj

added def CategoryTheory.monoidalOfHasFiniteProducts

added def CategoryTheory.symmetricOfHasFiniteCoproducts

added def CategoryTheory.symmetricOfHasFiniteProducts