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 _ _)