Commit 2021-05-18 16:02 a51d1e0e

View on Github →

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.

Estimated changes

Modified src/algebra/homology/homological_complex.lean

added def cochain_complex.of

added theorem cochain_complex.of_X

added theorem cochain_complex.of_d

added theorem cochain_complex.of_d_ne

added def cochain_complex.of_hom