geom_sum_mul_add — Mathlib

English

As a corollary of the previous commuting lemma, (∑_{i=0}^{n-1} (x+1)^i) · x + 1 = (x+1)^n.

Русский

Следствие из леммы о commuting: (∑_{i=0}^{n-1} (x+1)^i) · x + 1 = (x+1)^n.

LaTeX

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

Lean4

theorem geom_sum_mul_add (x : R) (n : ℕ) : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n :=
  by
  have := (Commute.one_right x).geom_sum₂_mul_add n
  rw [one_pow, geom_sum₂_with_one] at this
  exact this

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