Mathlib v3 is deprecated. Go to Mathlib v4

Def homotopy.mk_coinductive_aux₁

Modification history

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