mul_geom_sum₂_Ico — Mathlib

English

Let x, y ∈ R (R a commutative ring) and integers m ≤ n. Then (x − y) · ∑_{i ∈ Ico(m,n)} x^{i} y^{n−1−i} = x^{n} − x^{m} y^{n−m}.

Русский

Пусть x, y ∈ R и m ≤ n. Тогда (x − y) · ∑_{i ∈ Ico(m,n)} x^{i} y^{n−1−i} = x^{n} − x^{m} y^{n−m}.

LaTeX

$$$$ (x - y) \sum_{i \in \mathrm{Ico}(m,n)} x^{i} y^{n-1-i} = x^{n} - x^{m} y^{n-m} $$$$

Lean4

theorem mul_geom_sum₂_Ico (x y : R) {m n : ℕ} (hmn : m ≤ n) :
    ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m) :=
  (Commute.all x y).mul_geom_sum₂_Ico hmn

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