Mathlib Changelog
Changelog
About
Github
Commit
2020-07-11 10:11
34d3fe1d
View on Github →
chore(category_theory/comma): split into three files (
#3358
) Just reorganisation.
Estimated changes
Created
src/category_theory/arrow.lean
added
def
category_theory.arrow.hom_mk'
added
def
category_theory.arrow.hom_mk
added
theorem
category_theory.arrow.id_left
added
theorem
category_theory.arrow.id_right
added
theorem
category_theory.arrow.lift.fac_left
added
theorem
category_theory.arrow.lift.fac_right
added
def
category_theory.arrow.lift
added
theorem
category_theory.arrow.lift_mk'_left
added
theorem
category_theory.arrow.lift_mk'_right
added
def
category_theory.arrow.mk
added
theorem
category_theory.arrow.w
added
def
category_theory.arrow
Modified
src/category_theory/comma.lean
deleted
def
category_theory.arrow.hom_mk'
deleted
def
category_theory.arrow.hom_mk
deleted
theorem
category_theory.arrow.id_left
deleted
theorem
category_theory.arrow.id_right
deleted
theorem
category_theory.arrow.lift.fac_left
deleted
theorem
category_theory.arrow.lift.fac_right
deleted
def
category_theory.arrow.lift
deleted
theorem
category_theory.arrow.lift_mk'_left
deleted
theorem
category_theory.arrow.lift_mk'_right
deleted
def
category_theory.arrow.mk
deleted
theorem
category_theory.arrow.w
deleted
def
category_theory.arrow
deleted
theorem
category_theory.over.comp_left
deleted
def
category_theory.over.forget
deleted
theorem
category_theory.over.forget_map
deleted
theorem
category_theory.over.forget_obj
deleted
def
category_theory.over.hom_mk
deleted
theorem
category_theory.over.id_left
deleted
def
category_theory.over.iterated_slice_backward
deleted
theorem
category_theory.over.iterated_slice_backward_forget_forget
deleted
def
category_theory.over.iterated_slice_equiv
deleted
def
category_theory.over.iterated_slice_forward
deleted
theorem
category_theory.over.iterated_slice_forward_forget
deleted
def
category_theory.over.map
deleted
theorem
category_theory.over.map_map_left
deleted
theorem
category_theory.over.map_obj_hom
deleted
theorem
category_theory.over.map_obj_left
deleted
def
category_theory.over.mk
deleted
theorem
category_theory.over.mk_hom
deleted
theorem
category_theory.over.mk_left
deleted
theorem
category_theory.over.over_morphism.ext
deleted
theorem
category_theory.over.over_right
deleted
def
category_theory.over.post
deleted
theorem
category_theory.over.w
deleted
def
category_theory.over
deleted
theorem
category_theory.under.comp_right
deleted
def
category_theory.under.forget
deleted
theorem
category_theory.under.forget_map
deleted
theorem
category_theory.under.forget_obj
deleted
def
category_theory.under.hom_mk
deleted
theorem
category_theory.under.id_right
deleted
def
category_theory.under.map
deleted
theorem
category_theory.under.map_map_right
deleted
theorem
category_theory.under.map_obj_hom
deleted
theorem
category_theory.under.map_obj_right
deleted
def
category_theory.under.mk
deleted
def
category_theory.under.post
deleted
theorem
category_theory.under.under_left
deleted
theorem
category_theory.under.under_morphism.ext
deleted
theorem
category_theory.under.w
deleted
def
category_theory.under
Modified
src/category_theory/elements.lean
Modified
src/category_theory/limits/over.lean
Modified
src/category_theory/limits/shapes/strong_epi.lean
Created
src/category_theory/over.lean
added
theorem
category_theory.over.comp_left
added
def
category_theory.over.forget
added
theorem
category_theory.over.forget_map
added
theorem
category_theory.over.forget_obj
added
def
category_theory.over.hom_mk
added
theorem
category_theory.over.id_left
added
def
category_theory.over.iterated_slice_backward
added
theorem
category_theory.over.iterated_slice_backward_forget_forget
added
def
category_theory.over.iterated_slice_equiv
added
def
category_theory.over.iterated_slice_forward
added
theorem
category_theory.over.iterated_slice_forward_forget
added
def
category_theory.over.map
added
theorem
category_theory.over.map_map_left
added
theorem
category_theory.over.map_obj_hom
added
theorem
category_theory.over.map_obj_left
added
def
category_theory.over.mk
added
theorem
category_theory.over.mk_hom
added
theorem
category_theory.over.mk_left
added
theorem
category_theory.over.over_morphism.ext
added
theorem
category_theory.over.over_right
added
def
category_theory.over.post
added
theorem
category_theory.over.w
added
def
category_theory.over
added
theorem
category_theory.under.comp_right
added
def
category_theory.under.forget
added
theorem
category_theory.under.forget_map
added
theorem
category_theory.under.forget_obj
added
def
category_theory.under.hom_mk
added
theorem
category_theory.under.id_right
added
def
category_theory.under.map
added
theorem
category_theory.under.map_map_right
added
theorem
category_theory.under.map_obj_hom
added
theorem
category_theory.under.map_obj_right
added
def
category_theory.under.mk
added
def
category_theory.under.post
added
theorem
category_theory.under.under_left
added
theorem
category_theory.under.under_morphism.ext
added
theorem
category_theory.under.w
added
def
category_theory.under