Mathlib v3 is deprecated. Go to Mathlib v4

Theorem homotopy.prev_d_succ_cochain_complex

Modification history

2022-03-08 08:30
src/algebra/homology/homotopy.lean
feat(algebra/homology/homotopy) : `mk_coinductive` (#12457) …
Added homotopy.prev_d_succ_cochain_complexView on Github →