exists_prime_orderOf_dvd_card' — Mathlib

English

A variant of Cauchy’s theorem for finite groups can be derived via multiplicative to additive correspondence.

Русский

Вариант теоремы Коши для конечных групп выводится через эквивариантность умножения и сложения.

LaTeX

$$exists_prime_orderOf_dvd_card'$$

Lean4

/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
`p` in `G`. This is known as Cauchy's theorem. -/
@[to_additive]
theorem _root_.exists_prime_orderOf_dvd_card' {G : Type*} [Group G] [Finite G] (p : ℕ) [hp : Fact p.Prime]
    (hdvd : p ∣ Nat.card G) : ∃ x : G, orderOf x = p :=
  by
  have := Fintype.ofFinite G
  rw [Nat.card_eq_fintype_card] at hdvd
  exact exists_prime_orderOf_dvd_card p hdvd

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