geom_sum_Ico_mul_neg — Mathlib

English

For x and y commuting and m ≤ n, ∑_{i ∈ Ico m n} x^i times (1 − x) equals x^m − x^n.

Русский

Для коммутируемых x, y и m ≤ n сумма по Ico умноженная на (1 − x) даёт x^m − x^n.

LaTeX

$$$\\displaystyle \\left(\\sum_{i \\in \\mathrm{Ico}(m,n)} x^i\\right) (1 - x) = x^m - x^n$$$

Lean4

theorem geom_sum_Ico_mul_neg (x : R) {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n := by
  rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]

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