mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(topology/homotopy/H_spaces): define H spaces

Open faenuccio opened this issue 3 years ago • 0 comments

introduce H-spaces and prove basic properties, in particular that every topological group is a H-space and that the path space at a point is a H-space.

  • depends on: #15721 Open in Gitpod

faenuccio avatar Aug 12 '22 12:08 faenuccio