Hopf problem: main theorem · core 1

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

theorem Mathoverflow1973.complexManifold_isRealManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] (M : Type u_2) [TopologicalSpace M] [ChartedSpace E M] (n : WithTop ℕ∞) [IsManifold (modelWithCornersSelf ℂ E) n M] : IsManifold (modelWithCornersSelf ℝ E) n M