feat(topology/homotopy/H_spaces): define H spaces (#16029)
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.
Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
