odd_card_of_involutive — Mathlib

English

If a finite group G admits a fixed-point-free involutive endomorphism φ, then the cardinality of G is odd.

Русский

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

LaTeX

$$$\\text{Odd}(\\lvert G\\rvert)$$$

Lean4

theorem odd_card_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) : Odd (Nat.card G) :=
  by
  have := Fintype.ofFinite G
  by_contra h
  rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at h
  obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h
  exact hφ.orderOf_ne_two_of_involutive h2 g hg

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