Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-04-14 23:14
e4843ea0
View on Github →
chore(category_theory/subobject): split off specific subobjects (
#7167
)
Estimated changes
Modified
src/category_theory/subobject/factor_thru.lean
deleted
def
category_theory.limits.equalizer_subobject
deleted
theorem
category_theory.limits.equalizer_subobject_arrow'
deleted
theorem
category_theory.limits.equalizer_subobject_arrow
deleted
theorem
category_theory.limits.equalizer_subobject_arrow_comp
deleted
theorem
category_theory.limits.equalizer_subobject_factors
deleted
theorem
category_theory.limits.equalizer_subobject_factors_iff
deleted
def
category_theory.limits.equalizer_subobject_iso
deleted
def
category_theory.limits.factor_thru_image_subobject
deleted
def
category_theory.limits.image_subobject
deleted
theorem
category_theory.limits.image_subobject_arrow'
deleted
theorem
category_theory.limits.image_subobject_arrow
deleted
theorem
category_theory.limits.image_subobject_arrow_comp
deleted
theorem
category_theory.limits.image_subobject_factors_comp_self
deleted
def
category_theory.limits.image_subobject_iso
deleted
theorem
category_theory.limits.image_subobject_iso_comp
deleted
theorem
category_theory.limits.image_subobject_le
deleted
theorem
category_theory.limits.image_subobject_le_mk
deleted
def
category_theory.limits.image_subobject_map
deleted
theorem
category_theory.limits.image_subobject_map_arrow
deleted
def
category_theory.limits.kernel_subobject
deleted
theorem
category_theory.limits.kernel_subobject_arrow'
deleted
theorem
category_theory.limits.kernel_subobject_arrow
deleted
theorem
category_theory.limits.kernel_subobject_arrow_comp
deleted
theorem
category_theory.limits.kernel_subobject_comp_mono
deleted
theorem
category_theory.limits.kernel_subobject_factors
deleted
theorem
category_theory.limits.kernel_subobject_factors_iff
deleted
def
category_theory.limits.kernel_subobject_iso
deleted
theorem
category_theory.limits.le_kernel_subobject
Created
src/category_theory/subobject/limits.lean
added
def
category_theory.limits.equalizer_subobject
added
theorem
category_theory.limits.equalizer_subobject_arrow'
added
theorem
category_theory.limits.equalizer_subobject_arrow
added
theorem
category_theory.limits.equalizer_subobject_arrow_comp
added
theorem
category_theory.limits.equalizer_subobject_factors
added
theorem
category_theory.limits.equalizer_subobject_factors_iff
added
def
category_theory.limits.equalizer_subobject_iso
added
def
category_theory.limits.factor_thru_image_subobject
added
def
category_theory.limits.image_subobject
added
theorem
category_theory.limits.image_subobject_arrow'
added
theorem
category_theory.limits.image_subobject_arrow
added
theorem
category_theory.limits.image_subobject_arrow_comp
added
theorem
category_theory.limits.image_subobject_factors_comp_self
added
def
category_theory.limits.image_subobject_iso
added
theorem
category_theory.limits.image_subobject_iso_comp
added
theorem
category_theory.limits.image_subobject_le
added
theorem
category_theory.limits.image_subobject_le_mk
added
def
category_theory.limits.image_subobject_map
added
theorem
category_theory.limits.image_subobject_map_arrow
added
def
category_theory.limits.kernel_subobject
added
theorem
category_theory.limits.kernel_subobject_arrow'
added
theorem
category_theory.limits.kernel_subobject_arrow
added
theorem
category_theory.limits.kernel_subobject_arrow_comp
added
theorem
category_theory.limits.kernel_subobject_comp_mono
added
theorem
category_theory.limits.kernel_subobject_factors
added
theorem
category_theory.limits.kernel_subobject_factors_iff
added
def
category_theory.limits.kernel_subobject_iso
added
theorem
category_theory.limits.le_kernel_subobject