Mathlib Changelog
v4
Changelog
About
Github
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