Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_group.one_eq_H_space_e

Modification history

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