Hopf problem: recognition · degree 3

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

theorem Mathoverflow1973.MorseCancel.mul_transvection_surjective {r n : ℕ} (A : Matrix (Fin r) (Fin n) ℤ) (i j : Fin n) (hij : i ≠ j) (k : ℤ) (hA : Function.Surjective A.mulVec) : Function.Surjective (A * Matrix.transvection i j k).mulVec