cyclotomic_prime — Mathlib

English

If p is a prime, then Φ_p(R) = ∑ i ∈ range p, X^i.

Русский

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

LaTeX

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

Lean4

/-- If `p` is prime, then `cyclotomic p R = ∑ i ∈ range p, X ^ i`. -/
theorem cyclotomic_prime (R : Type*) [Ring R] (p : ℕ) [hp : Fact p.Prime] :
    cyclotomic p R = ∑ i ∈ Finset.range p, X ^ i :=
  by
  suffices cyclotomic p ℤ = ∑ i ∈ range p, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      congr_arg (map (Int.castRingHom R)) this
  rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors, erase_insert (mem_singleton.not.2 hp.out.ne_one.symm),
    prod_singleton]

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