English
Let P be the minimal polynomial of μ and Q be the minimal polynomial of μ^p, with p prime not dividing n. Then the reduction modulo p of P divides the reduction modulo p of Q.
Русский
Пусть P — минимальный полином μ, Q — минимальный полином μ^p, где p — простое и не делит n. Тогда редукция P по p делит редукцию Q по p.
LaTeX
$$$\operatorname{map}(\operatorname{Int.castRingHom}(\mathbb{Z}/p\mathbb{Z}))\left(\minpoly_{\mathbb{Z}}(\mu)\right) \mid \operatorname{map}(\operatorname{Int.castRingHom}(\mathbb{Z}/p\mathbb{Z}))\left(\minpoly_{\mathbb{Z}}(\mu^{p})\right)$$
Lean4
/-- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `Q` modulo `p`. -/
theorem minpoly_dvd_mod_p {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) :=
(squarefree_minpoly_mod h hdiv).isRadical _ _ (minpoly_dvd_pow_mod h hdiv)
