Commit 2025-04-15 13:58 14e33038

View on Github →

feat(CategoryTheory): ChosenFiniteProducts (Over X) (#21399) From Toric

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ChosenFiniteProducts/Over.lean

added theorem CategoryTheory.Over.associator_hom_left_fst

added theorem CategoryTheory.Over.associator_hom_left_snd_fst

added theorem CategoryTheory.Over.associator_hom_left_snd_snd

added theorem CategoryTheory.Over.associator_inv_left_fst_fst

added theorem CategoryTheory.Over.associator_inv_left_fst_snd

added theorem CategoryTheory.Over.associator_inv_left_snd

added theorem CategoryTheory.Over.braiding_hom_left

added theorem CategoryTheory.Over.braiding_inv_left

added def CategoryTheory.Over.chosenFiniteProducts

added theorem CategoryTheory.Over.leftUnitor_hom_left

added theorem CategoryTheory.Over.leftUnitor_inv_left_fst

added theorem CategoryTheory.Over.leftUnitor_inv_left_snd

added theorem CategoryTheory.Over.lift_left

added theorem CategoryTheory.Over.rightUnitor_hom_left

added theorem CategoryTheory.Over.rightUnitor_inv_left_fst

added theorem CategoryTheory.Over.rightUnitor_inv_left_snd

added theorem CategoryTheory.Over.tensorHom_left

added theorem CategoryTheory.Over.tensorHom_left_fst

added theorem CategoryTheory.Over.tensorHom_left_snd

added theorem CategoryTheory.Over.tensorObj_ext

added theorem CategoryTheory.Over.tensorObj_hom

added theorem CategoryTheory.Over.tensorObj_left

added theorem CategoryTheory.Over.tensorUnit_hom

added theorem CategoryTheory.Over.tensorUnit_left

added theorem CategoryTheory.Over.toUnit_left

added theorem CategoryTheory.Over.whiskerLeft_left

added theorem CategoryTheory.Over.whiskerLeft_left_fst

added theorem CategoryTheory.Over.whiskerLeft_left_snd

added theorem CategoryTheory.Over.whiskerRight_left

added theorem CategoryTheory.Over.whiskerRight_left_fst

added theorem CategoryTheory.Over.whiskerRight_left_snd