English
For a ring R, 0 < n and polynomial P over R, P = Φ_n R iff P multiplied by the product of Φ_i R over proper divisors of n equals X^n − 1.
Русский
Для кольца R, 0 < n и многочлена P над R: P = Φ_n R тогда и только тогда, когда P умножить на произведение Φ_i R по всем правильным делителям 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
theorem eq_cyclotomic_iff {R : Type*} [CommRing R] {n : ℕ} (hpos : 0 < n) (P : R[X]) :
P = cyclotomic n R ↔ (P * ∏ i ∈ Nat.properDivisors n, Polynomial.cyclotomic i R) = X ^ n - 1 :=
by
nontriviality R
refine ⟨fun hcycl => ?_, fun hP => ?_⟩
· rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← 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 [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]
refine ⟨by rwa [zero_add, mul_comm], ?_⟩
rw [degree_zero, bot_lt_iff_ne_bot]
intro h
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
