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