isCyclic_of_card_dvd_prime — Mathlib

English

If Nat.card α divides a prime p, then α is cyclic.

Русский

Если card(α) делит простое p, то α циклична.

LaTeX

$$$Nat.card(\\alpha) \\mid p \\Rightarrow IsCyclic(\\alpha) \text{ (with } p \text{ prime)}$$$

Lean4

/-- A finite group of order dividing a prime is cyclic. -/
@[to_additive /-- A finite group of order dividing a prime is cyclic. -/
    ]
theorem isCyclic_of_card_dvd_prime {p : ℕ} [hp : Fact p.Prime] (h : Nat.card α ∣ p) : IsCyclic α :=
  by
  rcases (Nat.dvd_prime hp.out).mp h with h | h
  · exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1
  · exact isCyclic_of_prime_card h

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