geom_sum₂_mul_add — Mathlib

English

In a commutative semiring, the generalized geometric-sum identity with x+y holds: (∑ i=0^{n-1} (x+y)^i) · x + y^n = (x+y)^n.

Русский

В коммутативном полугруппе с единицей верна общая тождество геометрической суммы с x+y: (∑ i=0^{n-1} (x+y)^i) · x + y^n = (x+y)^n.

LaTeX

$$$\\left(\\sum_{i=0}^{n-1} (x+y)^{i}\\right) \\cdot x + y^{n} = (x+y)^{n}$$$

Lean4

/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
theorem geom_sum₂_mul_add (x y : R) (n : ℕ) :
    (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n :=
  (Commute.all x y).geom_sum₂_mul_add n

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