Commit 2025-11-16 17:26 19f3ff9c

View on Github →

chore: deprecate monoidalOfHasFiniteProducts (#30684) Over the summer, this was replaced everywhere with CartesianMonoidalCategory.ofHasFiniteProducts, but hadn't been deprecated.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_fst

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_snd

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_snd

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_inv

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_inv

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorHom

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorUnit

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.unit_ext

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerLeft

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerRight

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq

modified theorem CategoryTheory.monoidalOfHasFiniteProducts.η_eq

modified def CategoryTheory.symmetricOfHasFiniteProducts