English
Let R be a nontrivial ring and n a natural number. Then the degree of the cyclotomic polynomial Φ_n over R is φ(n), where φ is Euler's totient function.
Русский
Пусть R — ненулевое кольцо, а n — натуральное. Тогда deg Φ_n над R равна φ(n), где φ — функция Эйлера-тотентий.
LaTeX
$$$$\deg(\mathrm{cyclotomic}\ n\ R) = \varphi(n).$$$$
Lean4
/-- The degree of `cyclotomic n` is `totient n`. -/
theorem degree_cyclotomic (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] : (cyclotomic n R).degree = Nat.totient n :=
by
rw [← map_cyclotomic_int]
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]
· rcases n with - | k
· simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero]
rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]
exact (int_cyclotomic_spec k.succ).2.1
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne, not_false_iff,
one_ne_zero]
