no goals
α : Type ?u.713413
inst✝³ : Fintype α
G✝ : Type ?u.713419
inst✝² : Group G✝
n : ℕ
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card (Multiplicative G)
convert hdvd