Mathlib v3 is deprecated. Go to Mathlib v4

Theorem path.delay_refl_left_one

Modification history

2023-05-23 19:44
src/topology/homotopy/H_spaces.lean
feat(topology/homotopy/H_spaces): define H spaces (#16029) …
Added path.delay_refl_left_oneView on Github →