Hopf problem: main theorem · core 2

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

@[reducible, inline]

abbrev Mathoverflow1973.unitSphere (n : ℕ) : Set (EuclideanSpace ℝ (Fin (n + 1)))

The unit n-sphere in Euclidean (n+1)-space.

Equations

• Mathoverflow1973.unitSphere n = Metric.sphere 0 1