English
If n = p^k with p prime, Φ_{p^k}(R) can be expressed as a Möbius-inverted product of X^p^j − 1 across j.
Русский
Если n = p^k с простым p, Φ_{p^k}(R) выразимо через произведение вида Möbius-инверсии над X^{p^j} − 1.
LaTeX
$$$$\mathrm{cyclotomic}\ (p^k)\ R = \prod_{j=0}^{k-1} (X^{p^j} - 1)^{\mu(p^{k-1-j})}$$$$
Lean4
/-- If `p ^ k` is a prime power, then
`cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ (p ^ n)) ^ i`. -/
theorem cyclotomic_prime_pow_eq_geom_sum {R : Type*} [CommRing R] {p n : ℕ} (hp : p.Prime) :
cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ n) ^ i :=
by
have :
∀ m,
(cyclotomic (p ^ (m + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) ↔
((∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) * ∏ x ∈ Finset.range (m + 1), cyclotomic (p ^ x) R) =
X ^ p ^ (m + 1) - 1 :=
by
intro m
have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i) (pow_pos hp.pos (m + 1))
rw [eq_comm] at this
rw [this, Nat.prod_properDivisors_prime_pow hp]
induction n with
| zero => haveI := Fact.mk hp; simp [cyclotomic_prime]
| succ n_n n_ih =>
rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]
rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
rw [this] at n_ih
rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]
simp only [pow_add, pow_one]
