Mathlib v3 is deprecated. Go to Mathlib v4

Def homotopy.of_eq

Modification history

2021-06-19 23:38

src/algebra/homology/homotopy.lean

feat(algebra/homology/homotopy): flesh out the api a bit, add some simps (#7941)

Added homotopy.of_eq View on Github →