Commit 2025-03-06 18:14 03239f29

View on Github →

feat(CategoryTheory): lifting compositions with the second and first projections (#22636) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

added theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_hom

added theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_inv

added theorem CategoryTheory.ChosenFiniteProducts.lift_snd_comp_fst_comp