exists_prime_addOrderOf_dvd_card — Mathlib

English

For additive groups, the same result holds for the additive order.

Русский

Для аддитивных групп справедлива та же теорема для порядка по сложению.

LaTeX

$$exists_prime_addOrderOf_dvd_card p hdvd$$

Lean4

/-- For every prime `p` dividing the order of a finite additive group `G` there exists an element of
order `p` in `G`. This is the additive version of Cauchy's theorem. -/
theorem _root_.exists_prime_addOrderOf_dvd_card {G : Type*} [AddGroup G] [Fintype G] (p : ℕ) [Fact p.Prime]
    (hdvd : p ∣ Fintype.card G) : ∃ x : G, addOrderOf x = p :=
  @exists_prime_orderOf_dvd_card (Multiplicative G) _ _ _ _ (by convert hdvd)

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