English
For 0 < n and polynomial P over R, P equals Φ_n R iff P multiplied by the product of Φ_i R over all proper divisors of n equals X^n − 1.
Русский
Для n > 0 и многочлена P над R равносильно: P = Φ_n(R) тогда и только тогда, когда P умножить на произведение Φ_i(R) по всем properDivisors n даёт X^n − 1.
LaTeX
$$$$0 < n \Rightarrow P = \mathrm{cyclotomic}\ n\ R \iff P \cdot \Big(\prod_{i \in \mathrm{Nat.properDivisors}\ n} \mathrm{cyclotomic}\ i\ R\Big) = X^n - 1.$$$$
Lean4
/-- We have
`cyclotomic n R = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic i K)`. -/
theorem cyclotomic_eq_X_pow_sub_one_div {R : Type*} [CommRing R] {n : ℕ} (hpos : 0 < n) :
cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ Nat.properDivisors n, cyclotomic i R :=
by
nontriviality R
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos, ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
have prod_monic : (∏ i ∈ Nat.properDivisors n, cyclotomic i R).Monic :=
by
apply monic_prod_of_monic
intro i _
exact cyclotomic.monic i R
rw [(div_modByMonic_unique (cyclotomic n R) 0 prod_monic _).1]
simp only [degree_zero, zero_add]
constructor
· rw [mul_comm]
rw [bot_lt_iff_ne_bot]
intro h
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
