English
If ζ is a primitive root of order k in a domain R, then the number of primitive k-th roots in R equals φ(k), the Euler totient.
Русский
Если ζ — примитивный корень порядка k в домене R, то число примитивных корней порядка k равно φ(k).
LaTeX
$$$IsPrimitiveRoot(ζ,k) \Rightarrow |\operatorname{primitiveRoots}(k,R)| = \varphi(k)$$$
Lean4
/-- If an integral domain has a primitive `k`-th root of unity, then it has `φ k` of them. -/
theorem card_primitiveRoots {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) : #(primitiveRoots k R) = φ k :=
by
by_cases h0 : k = 0
· simp [h0]
have : NeZero k := ⟨h0⟩
symm
refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_
· simp only [and_imp, mem_filter, mem_range]
rintro i - hi
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)]
exact h.pow_of_coprime i hi.symm
· simp only [and_imp, mem_filter, mem_range]
rintro i hi - j hj - H
exact h.pow_inj hi hj H
· simp only [exists_prop, mem_filter, mem_range]
intro ξ hξ
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0), h.isPrimitiveRoot_iff] at hξ
rcases hξ with ⟨i, hin, hi, H⟩
exact ⟨i, ⟨hin, hi.symm⟩, H⟩
