odd_orderOf_of_involutive — Mathlib

English

Given the same hypotheses as above, every element g ∈ G has odd order; that is, order(g) is odd for all g.

Русский

При тех же предпосылках каждый элемент g ∈ G имеет нечётный порядок; порядок каждого элемента нечётен.

LaTeX

$$$\\forall g\\in G:\\; Odd(\\operatorname{order}(g))$$$

Lean4

theorem odd_orderOf_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) (g : G) : Odd (orderOf g) :=
  Odd.of_dvd_nat (hφ.odd_card_of_involutive h2) (orderOf_dvd_natCard g)

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