geom_sum₂_with_one

Mathlib.Algebra.Ring.GeomSum

URI: https://scilib.ai/kg/mathlib#geom_sum₂_with_one

← MathLib Explorer

English

A standard identity: sum i from 0 to n-1 of x^i · x^{n-1-i} equals n · x^{n-1}.

Русский

Стандартная тождество: сумма i=0..n-1 of x^i · x^{n-1-i} равна n · x^{n-1}.

LaTeX

$$$\\sum_{i=0}^{n-1} x^{i} \\cdot x^{n-1-i} = n \\cdot x^{n-1}$$$

Lean4

theorem geom_sum₂_with_one (x : R) (n : ℕ) : ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i :=
  sum_congr rfl fun i _ => by rw [one_pow, mul_one]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru