geom_sum₂_succ_eq — Mathlib

English

Let R be a commutative ring and x, y ∈ R. For every natural number n, the following identity holds: ∑_{i=0}^{n} x^{i} y^{n−i} = x^{n} + y · ∑_{i=0}^{n−1} x^{i} y^{n−1−i}.

Русский

Пусть R — коммутативное кольцо и x, y ∈ R. Для любого натурального n выполняется тождество: ∑_{i=0}^{n} x^{i} y^{n−i} = x^{n} + y · ∑_{i=0}^{n−1} x^{i} y^{n−1−i}.

LaTeX

$$$$ \sum_{i=0}^{n} x^{i} y^{n-i} = x^{n} + y \sum_{i=0}^{n-1} x^{i} y^{n-1-i} $$$$

Lean4

theorem geom_sum₂_succ_eq (x y : R) {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) :=
  (Commute.all x y).geom_sum₂_succ_eq

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