Hopf problem: recognition · smale 12

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

theorem Mathoverflow1973.Smale.HomologyTransport.ker_comp_span_singleton {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] (p : A →ₗ[R] B) (q : B →ₗ[R] C) (v : A) (hq : q.ker = R ∙ p v) : (q ∘ₗ p).ker = p.ker ⊔ R ∙ v