English
Let μ be a primitive n-th root of unity in a domain of characteristic zero. If p is a prime not dividing n, then the reduction modulo p of the minimal polynomial of μ is squarefree.
Русский
Пусть μ — примитивный корень единицы степени n в области характеристики 0. Если p — простое число, не делящее n, то редукция минимального многочлена μ по модулю p является квадратноразложимой (кратные корни отсутствуют).
LaTeX
$$$\operatorname{Squarefree}\left(\operatorname{map}\left(\operatorname{Int.castRingHom}(\mathbb{Z}/p\mathbb{Z})\right)\left(\minpoly_{\mathbb{Z}}(\mu)\right)\right)$$$
Lean4
/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is squarefree. -/
theorem squarefree_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
Squarefree (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)) :=
(separable_minpoly_mod h hdiv).squarefree
