Hopf problem: homology of x · triangle period family homology lattice

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

theorem Mathoverflow1973.ThreefoldHomologyFreeProducts.finrank_pi_int {ι : Type u_1} [Fintype ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module ℤ (M i)] [∀ (i : ι), Module.Free ℤ (M i)] [∀ (i : ι), Module.Finite ℤ (M i)] [piModule : Module ℤ ((i : ι) → M i)] : Module.finrank ℤ ((i : ι) → M i) = ∑ i : ι, Module.finrank ℤ (M i)