Def category_theory.normal_epi_of_normal_mono_unop

Modification history

2021-05-06 06:18
src/category_theory/limits/shapes/normal_mono.lean
feat(category_theory): the opposite of an abelian category is abelian (#7514)
Added category_theory.normal_epi_of_normal_mono_unopView on Github →