α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < φ (Fintype.card α)
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < card (filter (fun a => orderOf a = Fintype.card α) univ)
rw [card_orderOf_eq_totient_aux₂ hn dvd_rfl]
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < φ (Fintype.card α)
exact totient_pos (Fintype.card_pos_iff.2 ⟨1⟩)