English
Cyclotomic polynomials satisfy a Möbius-inversion type product formula in the field of fractions: algebraMap to RatFunc_R of cyclotomic is equal to a Möbius-weighted product of X^i − 1 factors.
Русский
Циклотоми́ческие многочлены удовлетворяют форму продукта через инверсию Моебиуса в полях дробей: отображение к RatFunc_R от cyclotomic равняется произведению факторов X^i − 1, возведённому в коэффициент Моебиуса.
LaTeX
$$$$\text{algebraMap}_{R}\big(\mathrm{cyclotomic}_n R\big) = \prod_{i \in n.divisorsAntidiagonal} \big(\mathrm{algebraMap}_{R[X]}(X^{i.snd} - 1)\big)^{\mu(i.fst)}.$$$$
Lean4
/-- `cyclotomic n R` can be expressed as a product in a fraction field of `R[X]`
using Möbius inversion. -/
theorem cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type*) [CommRing R] [IsDomain R] :
algebraMap _ (RatFunc R) (cyclotomic n R) =
∏ i ∈ n.divisorsAntidiagonal, algebraMap R[X] _ (X ^ i.snd - 1) ^ μ i.fst :=
by
rcases n.eq_zero_or_pos with (rfl | hpos)
· simp
have h :
∀ n : ℕ,
0 < n → (∏ i ∈ Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) = algebraMap _ _ (X ^ n - 1 : R[X]) :=
by
intro n hn
rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos] <;>
simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]
· simp [cyclotomic_ne_zero]
· intro n hn
apply Monic.ne_zero
apply monic_X_pow_sub_C _ (ne_of_gt hn)
