geom_sum_mul — Mathlib

English

Let x be any ring element. Then (1) the identity (1 + x + x^2 + ... + x^{n-1})(x − 1) = x^n − 1 holds.

Русский

Для любого элемента кольца верно: (1 + x + x^2 + ... + x^{n-1})(x − 1) = x^n − 1.

LaTeX

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

Lean4

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

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