English
Let P be the minimal polynomial of a primitive μ and Q be the minimal polynomial of μ^p, where p does not divide n. Then P divides the expansion of Q by p.
Русский
Пусть P — минимальный полином примитивного μ, а Q — минимальный полином μ^p, где p не делит n. Тогда P делит развёртывание Q на p.
LaTeX
$$$\minpoly_{\mathbb{Z}}(\mu) \mid \operatorname{expand}_{\mathbb{Z}}(p)\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 natural number that does not divide `n`. Then `P` divides `expand ℤ p Q`. -/
theorem minpoly_dvd_expand {p : ℕ} (hdiv : ¬p ∣ n) : minpoly ℤ μ ∣ expand ℤ p (minpoly ℤ (μ ^ p)) :=
by
rcases n.eq_zero_or_pos with (rfl | hpos)
· simp_all
letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
refine minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) ?_
rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X, eval_comp, eval_X_pow, ←
eval₂_eq_eval_map, ← aeval_def]
exact minpoly.aeval _ _
