Structures · Topology
HSpace
A topological space X is an H-space if it behaves like a (potentially non-associative)
topological group, but where the axioms for a group only hold up to homotopy.
- Defined in
- Mathlib.Topology.Homotopy.HSpaces
- Shape
- One type argument · adds hmul, e, hmul_e_e, eHmul, hmulE
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Path
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by6
Ancestors0
No ancestors.