Hopf problem: threefold · special periods 3

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

theorem Mathoverflow1973.SpecialPeriods.CoprodTorsion.coprod_commute_inr {A B : Type u} [Group A] [Group B] (a : B) (ha : a ≠ 1) (g : Monoid.Coprod A B) (h : Commute (Monoid.Coprod.inr a) g) : ∃ (b : B), g = Monoid.Coprod.inr b