Hopf problem: elliptic · core 5

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

theorem Mathoverflow1973.Elliptic.HigherHomology.shortExtension_normalized_boundary_ker {M : Type u_1} [AddCommGroup M] [modM : Module ℤ M] {B : Type u_2} [AddCommGroup B] [Module ℤ B] (d : M →ₗ[ℤ] B) (eB : B ≃ₗ[ℤ] ℤ) : (↑eB ∘ₗ d).ker = d.ker