Commit 2025-07-14 16:30 5338f341

View on Github →

feat(CategoryTheory): inv (μ F X Y) = δ F X Y (#27061) and other basic lemmas From Toric

Estimated changes

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

added theorem CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ

added theorem CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom

added theorem CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ

added theorem CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom

added theorem CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ

added theorem CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ

added theorem CategoryTheory.Functor.Monoidal.inv_δ

added theorem CategoryTheory.Functor.Monoidal.inv_ε

added theorem CategoryTheory.Functor.Monoidal.inv_η

added theorem CategoryTheory.Functor.Monoidal.inv_μ

added theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η

added theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ

added theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight

added theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom