Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-15 12:17 28909a89

View on Github →

feat(category_theory/commas): add simp-lemmas for comma categories (#503)

Estimated changes

Modified category_theory/comma.lean

added theorem category_theory.comma.comp_left

added theorem category_theory.comma.comp_right

added def category_theory.comma.map_left_comp

added theorem category_theory.comma.map_left_comp_hom_app_left

added theorem category_theory.comma.map_left_comp_hom_app_right

added theorem category_theory.comma.map_left_comp_inv_app_left

added theorem category_theory.comma.map_left_comp_inv_app_right

added def category_theory.comma.map_left_id

added theorem category_theory.comma.map_left_id_hom_app_left

added theorem category_theory.comma.map_left_id_hom_app_right

added theorem category_theory.comma.map_left_id_inv_app_left

added theorem category_theory.comma.map_left_id_inv_app_right

added theorem category_theory.comma.map_left_map_left

added theorem category_theory.comma.map_left_map_right

added theorem category_theory.comma.map_left_obj_hom

added theorem category_theory.comma.map_left_obj_left

added theorem category_theory.comma.map_left_obj_right

added def category_theory.comma.map_right_comp

added theorem category_theory.comma.map_right_comp_hom_app_left

added theorem category_theory.comma.map_right_comp_hom_app_right

added theorem category_theory.comma.map_right_comp_inv_app_left

added theorem category_theory.comma.map_right_comp_inv_app_right

added def category_theory.comma.map_right_id

added theorem category_theory.comma.map_right_id_hom_app_left

added theorem category_theory.comma.map_right_id_hom_app_right

added theorem category_theory.comma.map_right_id_inv_app_left

added theorem category_theory.comma.map_right_id_inv_app_right

added theorem category_theory.comma.map_right_map_left

added theorem category_theory.comma.map_right_map_right

added theorem category_theory.comma.map_right_obj_hom

added theorem category_theory.comma.map_right_obj_left

added theorem category_theory.comma.map_right_obj_right