geom_sum_zero

Mathlib.Algebra.Ring.GeomSum

URI: https://scilib.ai/kg/mathlib#geom_sum_zero

English

Sum of powers of zero over a finite range equals 0 if the range is empty, else 1.

Русский

Сумма степеней нуля по конечному диапазону равна 0, если диапазон пуст, иначе единице.

LaTeX

$$$\\sum_{i=0}^{n-1} 0^{i} = \\begin{cases}0,& n=0\\\\ 1,& n>0\\end{cases}$$$

Lean4

theorem geom_sum_zero (x : R) : ∑ i ∈ range 0, x ^ i = 0 :=
  rfl

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

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

Разделы

Аффилиация

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