cyclotomic_dvd_geom_sum_of_dvd — Mathlib

English

If d divides n and d ≠ 1, then Φ_d(R) divides the sum ∑_{i=0}^{n-1} X^i.

Русский

Если d делит n и d ≠ 1, то Φ_d(R) делит сумму ∑_{i=0}^{n-1} X^i.

LaTeX

$$$$d \mid n \ (d \neq 1) \;\Rightarrow\; \mathrm{cyclotomic}\ d\ R \;|\; \sum_{i=0}^{n-1} X^i.$$$$

Lean4

theorem cyclotomic_dvd_geom_sum_of_dvd (R) [Ring R] {d n : ℕ} (hdn : d ∣ n) (hd : d ≠ 1) :
    cyclotomic d R ∣ ∑ i ∈ Finset.range n, X ^ i :=
  by
  suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← prod_cyclotomic_eq_geom_sum hn]
  apply Finset.dvd_prod_of_mem
  simp [hd, hdn, hn.ne']

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