case pos
k : ℕ
h : k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k

case neg
k : ℕ
h : ¬k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k
k : ℕ
⊢ Finset.card (primitiveRoots k ℂ) = φ k
by_cases h : k = 0
no goals
case neg
k : ℕ
h : ¬k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k
exact (isPrimitiveRoot_exp k h).card_primitiveRoots
no goals
case pos
k : ℕ
h : k = 0
⊢ Finset.card (primitiveRoots k ℂ) = φ k
simp [h]