dvd_geom_sum₂_iff_of_dvd_sub' — Mathlib

English

A variant: if p ∣ x−y in a commutative ring, then the same divisibility equivalence holds with p ∣ ∑ x^i y^{n−1−i} and p ∣ n x^{n−1} after replacing x by y and adjusting exponents.

Русский

Уточнение: если p|x−y, то аналогичное условие делимости сохраняется при замене переменных и степеней, тeм более обобщенно

LaTeX

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

Lean4

theorem dvd_geom_sum₂_iff_of_dvd_sub' {x y p : R} (h : p ∣ x - y) :
    (p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) ↔ p ∣ n * x ^ (n - 1) := by
  rw [geom_sum₂_comm, dvd_geom_sum₂_iff_of_dvd_sub]; simpa using h.neg_right

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