English
If the ring R has characteristic p and p divides n, then the cyclotomic polynomial at n·p over R equals the p-th power of the cyclotomic polynomial at n over R.
Русский
Пусть кольцо R имеет характеристику p и p делит n. Тогда циклото-мический полином при аргументе n·p над R равен p-й степени циклотомиального полинома при n над R.
LaTeX
$$$$ \\operatorname{cyclotomic}(n p, R) = \\operatorname{cyclotomic}(n, R)^{p}. $$$$
Lean4
/-- If `R` is of characteristic `p` and `p ∣ n`, then
`cyclotomic (n * p) R = (cyclotomic n R) ^ p`. -/
theorem cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : Fact (Nat.Prime p)] [Ring R] [CharP R p]
(hn : p ∣ n) : cyclotomic (n * p) R = cyclotomic n R ^ p :=
by
letI : Algebra (ZMod p) R := ZMod.algebra _ _
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this,
Polynomial.map_pow]
rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand, cyclotomic_expand_eq_cyclotomic hp.out hn,
map_cyclotomic]
