orderOf_ne_two_of_involutive — Mathlib

English

Let G be a finite group with a fixed-point-free involutive endomorphism φ. Then for every element g ∈ G, the order of g is not equal to 2; that is, no element has order 2.

Русский

Пусть G — конечная группа с фикс-пункт-фри инволютивным эндоморфизмом φ. Тогда для каждого элемента g ∈ G порядок g не равен 2; ни один элемент не имеет порядка 2.

LaTeX

$$$\\forall g\\in G:\\; order(g) \\neq 2$$$

Lean4

theorem orderOf_ne_two_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) (g : G) : orderOf g ≠ 2 :=
  by
  intro hg
  have key : φ g = g := by rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
  rw [hφ g key, orderOf_one] at hg
  contradiction

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