English
For any 0 < n, in a commutative ring R, the product over all divisors i of n of Φ_i(R) equals X^n − 1.
Русский
Пусть 0 < n. В коммутативном кольце R произведение по всем делителям i числа n циклотоми́ческих Φ_i(R) равно X^n − 1.
LaTeX
$$$$0 < n \;\Rightarrow\; \prod_{i \mid n} \mathrm{cyclotomic}\ i\ R = X^n - 1.$$$
Lean4
/-- `∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1`. -/
theorem prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type*) [CommRing R] :
∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1 :=
by
have integer : ∏ i ∈ Nat.divisors n, cyclotomic i ℤ = X ^ n - 1 :=
by
apply map_injective (Int.castRingHom ℂ) Int.cast_injective
simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X, Polynomial.map_one,
Polynomial.map_sub]
exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer
