English
For any 0 < n and commutative ring R, the product over i in n.divisors.erase 1 of Φ_i(R) equals the geometric sum ∑_{i=0}^{n-1} X^i.
Русский
Для любого 0 < n и коммутативного кольца R произведение по i в n.divisors.erase 1 от Φ_i(R) равно геометрической сумме ∑_{i=0}^{n-1} X^i.
LaTeX
$$$$0 < n \Rightarrow \prod_{i \in n.divisors.erase 1} \mathrm{cyclotomic}\ i\ R = \sum_{i=0}^{n-1} X^i.$$$$
Lean4
theorem dvd_X_pow_sub_one (n : ℕ) (R : Type*) [Ring R] : cyclotomic n R ∣ X ^ n - 1 :=
by
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X] using
Polynomial.map_dvd (Int.castRingHom R) this
rcases n.eq_zero_or_pos with (rfl | hn)
· simp
rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')
