geom₂_sum_of_lt — Mathlib

English

If x < y in a semifield with order, then for every natural n, ∑_{i=0}^{n-1} x^i y^{n-1-i} = (y^n − x^n)/(y − x).

Русский

Пусть x < y в полупольной структуре с порядком; тогда для любого n выполнено равенство ∑_{i=0}^{n-1} x^i y^{n-1-i} = (y^n − x^n)/(y − x).

LaTeX

$$$\\sum_{i=0}^{n-1} x^i y^{n-1-i}=\\frac{y^n-x^n}{y-x}$ при $x

Lean4

theorem geom₂_sum_of_lt (h : x < y) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_le h.le n)

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