mathlib

e0467bd0 - feat(algebra.homology): homology f g w ≅ cokernel (kernel.lift g f w) (#8355)

feat(algebra.homology): homology f g w ≅ cokernel (kernel.lift g f w) (#8355) Per [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Challenge.20with.20homology). I'm not certain this completely resolves the issue: perhaps we should really change the definition of `homology`. But at least this bridges the gap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>