English
If N is nontrivial, the generalized homotopy group is a commutative group (Eckmann–Hilton).
Русский
Если N ненулевой, то обобщённая гомотопическая группа коммутирует (Eckmann–Hilton).
LaTeX
$$$\\text{If }\\mathrm{Nonempty}(N),\\; \\mathrm{HomotopyGroup}(N,X,x)\\; \\text{is a commutative group}$$$
Lean4
/-- Multiplication on `HomotopyGroup N X x` is commutative for nontrivial `N`.
In particular, multiplication on `π_(n+2)` is commutative. -/
instance commGroup [Nontrivial N] : CommGroup (HomotopyGroup N X x) :=
let h := exists_ne (Classical.arbitrary N)
@EckmannHilton.commGroup (HomotopyGroup N X x) _ 1 (isUnital_auxGroup <| Classical.choose h) _
(by
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩
apply congr_arg Quotient.mk'
simp only [fromLoop_trans_toLoop, transAt_distrib <| Classical.choose_spec h, coe_toEquiv, loopHomeo_apply,
coe_symm_toEquiv, loopHomeo_symm_apply])
