Hopf problem: homology of x · cusp coinvariants

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

theorem Mathoverflow1973.CuspCoinvariants.mem_range_iff_of_intertwines {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] (e : M ≃ₗ[ℤ] N) (A : M →ₗ[ℤ] M) (B : N →ₗ[ℤ] N) (h : ∀ (x : M), e (A x) = B (e x)) (x : M) : x ∈ A.range ↔ e x ∈ B.range