Hopf problem: recognition · smale 9 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Smale.LocalDegree.norm_radius_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(r : ℝ)
(hr : 0 < r)
(u : ↑(Metric.sphere 0 1))
: