Hopf problem: main theorem · six sphere cube 2

Supporting definitions and proofs for this stage of the six-sphere construction.

@[reducible, inline]

abbrev Mathoverflow1973.SixSphereCube.StandardSphere : Set (EuclideanSpace ℝ (Fin (6 + 1)))

The standard unit six-sphere.

Equations

• Mathoverflow1973.SixSphereCube.StandardSphere = Mathoverflow1973.SphereHomology.UnitSphere 6