eval_geom_sum — Mathlib

English

The evaluation of a geometric sum of the monomial X by x equals the geometric sum of powers of x: eval x (sum_{i=0}^{n-1} X^i) = sum_{i=0}^{n-1} x^i.

Русский

Оценивание геометрической суммы монома X даёт геометрическую сумму степеней x: eval x (sum_{i=0}^{n-1} X^i) = sum_{i=0}^{n-1} x^i.

LaTeX

$$$\\operatorname{eval}\\ x\\; \\bigg( \\sum_{i=0}^{n-1} X^i \\bigg) = \\sum_{i=0}^{n-1} x^i$$$

Lean4

@[simp]
theorem eval_geom_sum {R} [CommSemiring R] {n : ℕ} {x : R} : eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i := by
  simp [eval_finset_sum]

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