Hopf problem: recognition · smale 5

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

theorem Mathoverflow1973.Smale.FrameField.isInvertible_coprod_of_bijective {D : Type u_1} {Z : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ D] [FiniteDimensional ℝ Z] (G : D →L[ℝ] F) (C : Z →L[ℝ] F) (h : Function.Bijective ⇑(G.coprod C)) : (G.coprod C).IsInvertible