no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd