Commit 2024-01-27 14:51 f1919fd4

View on Github →

feat(CategoryTheory/Monoidal): add lemmas for the whiskerings (#9995) Extracted from #6307.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Basic.lean

deleted theorem CategoryTheory.Bicategory.hom_inv_whiskerLeft

deleted theorem CategoryTheory.Bicategory.inv_hom_whiskerLeft

added theorem CategoryTheory.Bicategory.whiskerLeft_hom_inv

added theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom

Modified Mathlib/CategoryTheory/Bicategory/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

added theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight'

added theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight

added theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight'

added theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight

added theorem CategoryTheory.MonoidalCategory.inv_whiskerLeft

added theorem CategoryTheory.MonoidalCategory.inv_whiskerRight

added def CategoryTheory.MonoidalCategory.whiskerLeftIso

added theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv'

added theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv

added theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom'

added theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom

added def CategoryTheory.MonoidalCategory.whiskerRightIso

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

added theorem CategoryTheory.Center.whiskerLeft_f

added theorem CategoryTheory.Center.whiskerRight_f

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight

added theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerLeft

added theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerRight

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean