Commit 2024-03-06 21:35 35909eaa

View on Github →

chore(CategoryTheory/MonoidalCategory): split the monoidal composition (#11149) I realized that the monoid composition ⊗≫ can be defined without depending on the free monoid category, and that it is still useful.

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

deleted def Mathlib.Tactic.Coherence.monoidalComp

deleted theorem Mathlib.Tactic.Coherence.monoidalComp_refl

deleted def Mathlib.Tactic.Coherence.monoidalIso

Created Mathlib/Tactic/CategoryTheory/MonoidalComp.lean

added def CategoryTheory.monoidalComp

added theorem CategoryTheory.monoidalComp_refl

added def CategoryTheory.monoidalIso

added def CategoryTheory.monoidalIsoComp

Modified scripts/noshake.json

Created test/CategoryTheory/MonoidalComp.lean