Cyclic_Groups_of_Order_p_q
Provedcyclic-groupsgroup-theoryprimesproofwiki
Let p, q be primes with p < q and p does not divide q-1. Then every group of order pq is cyclic.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic -- If p, q are primes with p < q and p does not divide q-1, -- then every group of order pq is cyclic. theorem Cyclic_Groups_of_Order_p_q (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) (hndvd : ¬ p ∣ (q - 1)) (G : Type _) [Group G] [Fintype G] (hG : Fintype.card G = p * q) : IsCyclic G := by sorry
Source