Commit 2024-10-15 23:57 c63a0ac5

View on Github →

chore(CategoryTheory/ChosenFiniteProducts): port some simp lemmas from CategoryTheory/Limits/Shapes/BinaryProducts (#17733)

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

added theorem CategoryTheory.ChosenFiniteProducts.comp_lift

added theorem CategoryTheory.ChosenFiniteProducts.lift_fst_comp_snd_comp

added theorem CategoryTheory.ChosenFiniteProducts.lift_fst_snd

added theorem CategoryTheory.ChosenFiniteProducts.lift_map