Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-06 06:18
7040c50c
View on Github →
feat(category_theory): the opposite of an abelian category is abelian (
#7514
)
Estimated changes
Created
src/category_theory/abelian/opposite.lean
Modified
src/category_theory/fin_category.lean
added
def
category_theory.fin_category_opposite
Modified
src/category_theory/limits/opposites.lean
added
theorem
category_theory.limits.has_finite_colimits_opposite
added
theorem
category_theory.limits.has_finite_coproducts_opposite
added
theorem
category_theory.limits.has_finite_limits_opposite
added
theorem
category_theory.limits.has_finite_products_opposite
Modified
src/category_theory/limits/shapes/normal_mono.lean
added
def
category_theory.normal_epi_of_normal_mono_unop
added
def
category_theory.normal_mono_of_normal_epi_unop
Modified
src/category_theory/limits/shapes/zero.lean
Created
src/category_theory/preadditive/opposite.lean
added
theorem
category_theory.unop_add
added
theorem
category_theory.unop_zero