Commit 2024-02-02 06:26 007ad742

View on Github →

refactor(CategoryTheory/Monoidal/Braided): use monoidalComp in the proofs (#10078)

depends on: #10061

Estimated changes

Modified Mathlib/CategoryTheory/Monad/EquivMon.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

deleted theorem CategoryTheory.associator_monoidal_aux

added theorem CategoryTheory.braiding_tensorUnit_left

added theorem CategoryTheory.braiding_tensorUnit_right

deleted theorem CategoryTheory.tensor_associativity_aux

modified def CategoryTheory.tensor_μ

deleted theorem CategoryTheory.tensor_μ_def₁

deleted theorem CategoryTheory.tensor_μ_def₂

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

added def CategoryTheory.Center.whiskerLeft

added theorem CategoryTheory.Center.whiskerLeft_comm

added def CategoryTheory.Center.whiskerRight

added theorem CategoryTheory.Center.whiskerRight_comm

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.LaxMonoidalFunctor.associativity'

added theorem CategoryTheory.LaxMonoidalFunctor.associativity_inv'

added theorem CategoryTheory.LaxMonoidalFunctor.left_unitality'

added theorem CategoryTheory.LaxMonoidalFunctor.left_unitality_inv'

added theorem CategoryTheory.LaxMonoidalFunctor.right_unitality'

added theorem CategoryTheory.LaxMonoidalFunctor.right_unitality_inv'

added theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left'

added theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right'

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/CategoryTheory/Monoidal/Mod_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean