English
If there exists a primitive n-th root of unity in R, then the natural degree of cyclotomic' n R equals φ(n).
Русский
Если в кольце R существует примитивный корень n-й степени единицы ζ, то натуральная степень полинома cyclotomic' n R равна φ(n).
LaTeX
$$$\operatorname{natDegree}(\operatorname{cyclotomic}'(n,R)) = \operatorname{totient}(n)$$$
Lean4
/-- The natural degree of `cyclotomic' n R` is `totient n` if there is a primitive root of
unity in `R`. -/
theorem natDegree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).natDegree = Nat.totient n :=
by
rw [cyclotomic']
rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]
·
simp only [IsPrimitiveRoot.card_primitiveRoots h, mul_one, natDegree_X_sub_C, Nat.cast_id, Finset.sum_const,
nsmul_eq_mul]
intro z _
exact X_sub_C_ne_zero z
