Hopf problem: pi 1 · twist group

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

theorem Mathoverflow1973.TwistGroup.main_realization_generators_eq_one {G : Type u_1} [Group G] (c₀ x₀ y₀ : G) (hcx : Commute c₀ x₀) (hcy : Commute c₀ y₀) (hxy : x₀ * y₀ = 1) (hx : x₀ ^ 3 = c₀) (hy : y₀ ^ 4 = c₀⁻¹) : c₀ = 1 ∧ x₀ = 1 ∧ y₀ = 1