English
If a primitive n-th root exists in R, then the degree of cyclotomic' n R is φ(n).
Русский
Если существует примитивный корень n-й степени в R, то степень cyclotomic' n R равна φ(n).
LaTeX
$$$\operatorname{degree}(\operatorname{cyclotomic}'(n,R)) = \operatorname{totient}(n)$$$
Lean4
/-- The degree of `cyclotomic' n R` is `totient n` if there is a primitive root of unity in `R`. -/
theorem degree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).degree = Nat.totient n := by
simp only [degree_eq_natDegree (cyclotomic'_ne_zero n R), natDegree_cyclotomic' h]