Def CategoryTheory.monoidalOfHasFiniteProducts

Modification history

2023-08-07 12:37

Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

feat(CategoryTheory/Monoidal): define whiskering operators (#6420) …

Modified CategoryTheory.monoidalOfHasFiniteProducts View on Github →

2023-06-08 16:01

Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

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

Added CategoryTheory.monoidalOfHasFiniteProducts View on Github →