case mk.intro
α✝ : Type u
a : α✝
inst✝³ : Group α✝
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : IsAddCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
g : α
hg : ∀ (x : α), x ∈ AddSubgroup.zmultiples g
⊢ card (filter (fun a => addOrderOf a = d) univ) = φ d
α✝ : Type u
a : α✝
inst✝³ : Group α✝
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : IsAddCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => addOrderOf a = d) univ) = φ d
obtain ⟨g, hg⟩ := id ‹IsAddCyclic α›
no goals
case mk.intro
α✝ : Type u
a : α✝
inst✝³ : Group α✝
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : IsAddCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
g : α
hg : ∀ (x : α), x ∈ AddSubgroup.zmultiples g
⊢ card (filter (fun a => addOrderOf a = d) univ) = φ d
apply @IsCyclic.card_orderOf_eq_totient (Multiplicative α) _ ⟨⟨g, hg⟩⟩ (_) _ hd