dvd_geom_sum₂_self — Mathlib

English

If p divides x − y, then p divides the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1−i}. This is the special case when p divides the difference and certain conditions are met.

Русский

Если p делит x − y, то p делит геометрическую сумму ∑_{i=0}^{n-1} x^i y^{n-1−i}. Это частный случай при выполнении условий.

LaTeX

$$$p \mid (x-y) \Rightarrow p \mid \sum_{i=0}^{n-1} x^i y^{n-1-i}.$$$

Lean4

theorem dvd_geom_sum₂_self {x y : R} (h : ↑n ∣ x - y) : ↑n ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) :=
  (dvd_geom_sum₂_iff_of_dvd_sub h).mpr (dvd_mul_right _ _)

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