English
If R has characteristic p and p ∤ n, then cyclotomic(n p) R = (cyclotomic n R)^{p-1}.
Русский
Если характеристика кольца R равна p и p не делит n, тогда cyclotomic(n p) R = (cyclotomic n R)^{p-1}.
LaTeX
$$cyclotomic(n * p) R = cyclotomic(n, R) ^ (p - 1)$$
Lean4
/-- If `R` is of characteristic `p` and `¬p ∣ n`, then
`cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1)`. -/
theorem cyclotomic_mul_prime_eq_pow_of_not_dvd (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 - 1) :=
by
letI : Algebra (ZMod p) R := ZMod.algebra _ _
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this,
Polynomial.map_pow]
apply mul_right_injective₀ (cyclotomic_ne_zero n <| ZMod p); dsimp
rw [← pow_succ', tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]
conv_rhs => rw [← map_cyclotomic_int]
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul, map_cyclotomic, map_cyclotomic]
