Commit 2025-02-08 08:03 82c447be

View on Github →

feat(CategoryTheory): more API for ChosenFiniteProducts (#21509)

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

added theorem CategoryTheory.ChosenFiniteProducts.braiding_eq_braiding

added theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_fst

added theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_snd

added theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_fst

added theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_snd

added theorem CategoryTheory.ChosenFiniteProducts.lift_comp_fst_snd

added theorem CategoryTheory.ChosenFiniteProducts.lift_leftUnitor_hom

added theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_hom

added theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_inv

added theorem CategoryTheory.ChosenFiniteProducts.lift_rightUnitor_hom

added theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerLeft

added theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerRight

added theorem CategoryTheory.Functor.Monoidal.lift_δ

added theorem CategoryTheory.Functor.Monoidal.lift_μ

added theorem CategoryTheory.Functor.Monoidal.toUnit_ε

added theorem CategoryTheory.Functor.Monoidal.δ_fst

added theorem CategoryTheory.Functor.Monoidal.δ_snd

added theorem CategoryTheory.Functor.Monoidal.μ_fst

added theorem CategoryTheory.Functor.Monoidal.μ_snd

added theorem CategoryTheory.NatTrans.monoidal_of_preservesFiniteProducts

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

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd