Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-20 12:01 ab5d0f15

View on Github →

feat(category_theory/binary_products): some product lemmas and their dual (#2752) A bunch of lemmas about binary products.

Estimated changes

Modified src/category_theory/limits/shapes/binary_products.lean

added theorem category_theory.limits.braid_natural

modified theorem category_theory.limits.coprod.inl_map

modified theorem category_theory.limits.coprod.inr_map

added theorem category_theory.limits.coprod.map_desc

added theorem category_theory.limits.coprod_desc_inl_inr

added theorem category_theory.limits.coprod_map_comp_id

added theorem category_theory.limits.coprod_map_id_comp

added theorem category_theory.limits.coprod_map_id_id

added theorem category_theory.limits.coprod_map_map

added theorem category_theory.limits.prod.lift_map

modified theorem category_theory.limits.prod.map_fst

modified theorem category_theory.limits.prod.map_snd

modified theorem category_theory.limits.prod.symmetry'

modified theorem category_theory.limits.prod.symmetry

added def category_theory.limits.prod_functor_left_comp

added theorem category_theory.limits.prod_left_unitor_hom_naturality

added theorem category_theory.limits.prod_left_unitor_inv_naturality

added theorem category_theory.limits.prod_lift_fst_snd

added theorem category_theory.limits.prod_map_comp_id

added theorem category_theory.limits.prod_map_id_comp

added theorem category_theory.limits.prod_map_id_id

added theorem category_theory.limits.prod_map_map

added theorem category_theory.limits.prod_right_unitor_hom_naturality

added theorem category_theory.limits.prod_right_unitor_inv_naturality