Mathlib v3 is deprecated. Go to Mathlib v4

Theorem homotopy.d_next_cochain_complex

Modification history

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