Hopf problem: elliptic · core 8

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

theorem Mathoverflow1973.Elliptic.HigherHomology.triangularFinTwo_injective (F : (Fin 2 → ℤ) →ₗ[ℤ] Fin 2 → ℤ) (d : ℤ) (hfirst : F ![1, 0] = ![1, 0]) (hsecond : ∀ (v : Fin 2 → ℤ), F v 1 = d * v 1) (hd : d ≠ 0) : Function.Injective ⇑F