mathlib

a51d1e0e - feat(algebra/homology/homological_complex): Dualizes some constructions (#7643)

feat(algebra/homology/homological_complex): Dualizes some constructions (#7643) This PR adds `cochain_complex.of` and `cochain_complex.of_hom`. Still not done: `cochain_complex.mk`.