Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 17:25 5e36e121

View on Github →

feat(category_theory/abelian/homology): Adds API for homology mimicking that of (co)kernels. (#12171)

Estimated changes

added theorem homology.condition_ι
added theorem homology.condition_π'
added def homology.desc'
added theorem homology.hom_from_ext
added theorem homology.hom_to_ext
added def homology.lift
added theorem homology.lift_ι
added def homology.ι
added def homology.π'
added theorem homology.π'_desc'
added theorem homology.π'_eq_π
added theorem homology.π'_map
added theorem homology.π'_ι