commute_all_of_involutive — Mathlib

English

If G is a finite group and φ: G → G is a fixed-point-free involutive endomorphism, then every pair of elements g,h ∈ G commute; i.e., G is abelian.

Русский

Если G конечная группа и φ: G → G — фикс-пунктово-фри инволютивный эндоморфизм, тогда любые два элемента группы commute, то есть G абелева.

LaTeX

$$$\\forall G\\,[Group\\ G],\\,[Finite\\ G],\\forall \\varphi:\\,G\\to G,\\ FixedPointFree(\\varphi) \\land Involutive(\\varphi)\\Rightarrow \\forall g,h\\in G,\\ gh=hg$$$

Lean4

theorem commute_all_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) (g h : G) : Commute g h :=
  by
  have key := map_mul φ g h
  rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key

Похожие утверждения