geom₂_sum — Mathlib

English

For any field K and elements x,y with x ≠ y, the sum ∑ i ∈ range n of x^i · y^(n−1−i) equals (x^n − y^n)/(x − y).

Русский

Для поля K и элементов x,y с x ≠ y сумма ∑ i∈range n x^i y^(n−1−i) равна (x^n − y^n)/(x − y).

LaTeX

$$$\forall x,y\in K,\ x \neq y \Rightarrow \sum_{i=0}^{n-1} x^i y^{n-1-i} = \dfrac{x^n - y^n}{x - y}$$$

Lean4

theorem geom₂_sum (h : x ≠ y) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) :=
  (Commute.all x y).geom_sum₂ h n

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