English
If the ring R has characteristic p and p does not divide m, then cyclotomic(p^k · m) equals cyclotomic(m) raised to the power (p^k − p^(k−1)) for all k > 0.
Русский
Если характеристика кольца R равна p и p не делит m, то cyclotomic(p^k · m) = cyclotomic(m)^{p^k − p^{k−1}} для всех k > 0.
LaTeX
$$$$ \\operatorname{cyclotomic}(p^k m, R) = \\operatorname{cyclotomic}(m, R)^{\,p^k - p^{\,k-1}}. $$$$
Lean4
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then
`cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))`. -/
theorem cyclotomic_mul_prime_pow_eq (R : Type*) {p m : ℕ} [Fact (Nat.Prime p)] [Ring R] [CharP R p] (hm : ¬p ∣ m) :
∀ {k}, 0 < k → cyclotomic (p ^ k * m) R = cyclotomic m R ^ (p ^ k - p ^ (k - 1))
| 1, _ => by rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
| a + 2, _ => by
have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩
rw [pow_succ', mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv,
cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ← pow_mul]
· simp only [tsub_zero, Nat.succ_sub_succ_eq_sub]
rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]
· assumption
