Commit 2025-08-28 14:28 6c972550

View on Github →

feat: Mon_ C is cartesian-monoidal if C is (#25326) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

added theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_fst

added theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_snd

added theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_fst

added theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_snd

added theorem CategoryTheory.CartesianMonoidalCategory.toUnit_unit

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

added theorem Mon_.fst_hom

added theorem Mon_.lift_hom

added theorem Mon_.snd_hom