mul_geom_sum₂ — Mathlib

English

For commuting x and y in a ring, the product (x − y) times the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1-i} equals x^n − y^n.

Русский

Пусть x и y коммутируют в кольце; произведение (x − y) на геометрическую сумму ∑ x^i y^{n−1−i} дает x^n − y^n.

LaTeX

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

Lean4

theorem mul_geom_sum₂ (h : Commute x y) (n : ℕ) : ((x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = x ^ n - y ^ n :=
  by rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]

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