Commit 2022-03-08 08:30 b3fba033

View on Github →

feat(algebra/homology/homotopy) : mk_coinductive (#12457) mk_coinductive is the dual version of mk_inductive in the same file. mk_inductive is to build homotopy of chain complexes inductively and mk_coinductive is to build homotopy of cochain complexes inductively.

Estimated changes

Modified src/algebra/homology/homotopy.lean

added theorem homotopy.d_next_cochain_complex

added def homotopy.mk_coinductive

added def homotopy.mk_coinductive_aux₁

added def homotopy.mk_coinductive_aux₂

added theorem homotopy.mk_coinductive_aux₃

added theorem homotopy.prev_d_succ_cochain_complex

added theorem homotopy.prev_d_zero_cochain_complex