geom_sum_Ico_mul — Mathlib

English

For a ring R and x, with m ≤ n, the Ico-based sum times (x − 1) equals x^n − x^m.

Русский

Для кольца R и элемента x при m ≤ n сумма по Ico умноженная на (x − 1) даёт x^n − x^m.

LaTeX

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

Lean4

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

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