prod_cyclotomic_eq_geom_sum — Mathlib

English

If p is prime, then Φ_p(R) equals the sum of X^i for i = 0 to p−1.

Русский

Если p — простое число, то Φ_p(R) = ∑_{i=0}^{p-1} X^i.

LaTeX

$$$$\mathrm{cyclotomic}\ p\ R = \sum_{i=0}^{p-1} X^i.$$$$

Lean4

theorem prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R) [CommRing R] :
    ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ Finset.range n, X ^ i :=
  by
  suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
    simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      congr_arg (map (Int.castRingHom R)) this
  rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'), cyclotomic_one,
    geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]

Похожие утверждения