mathlib3
caf6f192 - refactor(category_theory/abelian): deduplicate definitions of (co)image (#12902)

Commit
4 years ago
refactor(category_theory/abelian): deduplicate definitions of (co)image (#12902) Previously we made two separate definitions of the abelian (co)image, as `kernel (cokernel.π f)` / `cokernel (kernel.ι f)`, once for `non_preadditive_abelian C` and once for `abelian C`. This duplication wasn't really necessary, and this PR unifies them. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading