English
Let P be the minimal polynomial of μ and Q the minimal polynomial of μ^p, with p a prime not dividing n. Then P divides the reduction modulo p of Q raised to p, i.e., P | (expand by p of Q) mod p.
Русский
Пусть P — минимальный полином μ и Q — минимальный полином μ^p при простом p, не делящем n. Тогда P делит редукцию по p на (expand p) от Q.
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)^{p}$$$
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 ^ p` modulo `p`. -/
theorem minpoly_dvd_pow_mod {p : ℕ} [hprime : Fact p.Prime] (hdiv : ¬p ∣ n) :
map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p :=
by
set Q := minpoly ℤ (μ ^ p)
have hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (expand ℤ p Q) := by
rw [← ZMod.expand_card, map_expand]
rw [hfrob]
apply _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
exact minpoly_dvd_expand h hdiv
