dvd_geom_sum₂_iff_of_dvd_sub — Mathlib

English

In a commutative ring, if p divides x − y, then p divides the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1−i} if and only if p divides n y^{n−1}.

Русский

В коммутативном кольце, если p делит x−y, тогда p делит геометрическую сумму ∑_{i=0}^{n−1} x^i y^{n−1−i} тогда и только тогда, когда p делит n y^{n−1}.

LaTeX

$$$p \mid (x-y) \Rightarrow\ (p \mid \sum_{i=0}^{n-1} x^i y^{n-1-i}) \iff (p \mid n y^{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 * y ^ (n - 1) :=
  by
  rw [← mem_span_singleton, ← Ideal.Quotient.eq] at h
  simp only [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, h, geom_sum₂_self, map_mul, map_pow,
    map_natCast]

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