Hopf problem: period family · core 9

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

theorem Mathoverflow1973.PeriodFamily.Boundary.ThirdRelation.circleMorphism_zero (G : Type) [TopologicalSpace G] [AddCommGroup G] (v : C(PeriodTorusHigherHomology.CircleTopology.Circle, G)) (hv : ∀ (x y : PeriodTorusHigherHomology.CircleTopology.Circle), v (x + y) = v x + v y) : v 0 = 0