geom_sum₂_mul — Mathlib

English

For any commutative ring R and any x, y, the geometric sum satisfies (sum) (x − y) = x^n − y^n.

Русский

Для коммутативного кольца R и любых x, y геометрическая сумма удовлетворяет (сумма) (x − y) = x^n − y^n.

LaTeX

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

Lean4

theorem geom_sum₂_mul (x y : R) (n : ℕ) : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n :=
  (Commute.all x y).geom_sum₂_mul n

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