12.2. Products
Mathlib knows that the product of two H-spaces is an H-space:
variable (H' : Type*) [TopologicalSpace H'] [HSpace H']
#synth HSpace (H × H')
Furthermore we can witness that the multiplication on the product is what we expect as follows:
example (x y : H) (x' y' : H') :
(x ⋀ y, x' ⋀ y') = (x, x') ⋀ (y, y') :=
rfl