Hopf problem: homology of x · threefold homology 1

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

theorem Mathoverflow1973.ThreefoldHomology.exact_of_linearEquiv_squares {A : Type u_1} {B : Type u_2} {C : Type u_3} {A' : Type u_4} {B' : Type u_5} {C' : Type u_6} [AddCommGroup A] [Module ℤ A] [AddCommGroup B] [Module ℤ B] [AddCommGroup C] [Module ℤ C] [AddCommGroup A'] [Module ℤ A'] [AddCommGroup B'] [Module ℤ B'] [AddCommGroup C'] [Module ℤ C'] (f : A →ₗ[ℤ] B) (g : B →ₗ[ℤ] C) (f' : A' →ₗ[ℤ] B') (g' : B' →ₗ[ℤ] C') (eA : A ≃ₗ[ℤ] A') (eB : B ≃ₗ[ℤ] B') (eC : C ≃ₗ[ℤ] C') (hf : f' ∘ₗ ↑eA = ↑eB ∘ₗ f) (hg : g' ∘ₗ ↑eB = ↑eC ∘ₗ g) (hexact : Function.Exact ⇑f ⇑g) : Function.Exact ⇑f' ⇑g'