geom_sum_two

Mathlib.Algebra.Ring.GeomSum

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

English

Sum over i in range 2 of x^i equals x + 1.

Русский

Сумма по i=0..1 степеней x равна x + 1.

LaTeX

$$$\\sum_{i=0}^{1} x^{i} = x + 1$$$

Lean4

@[simp]
theorem geom_sum_two {x : R} : ∑ i ∈ range 2, x ^ i = x + 1 := by simp [geom_sum_succ']

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

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

Разделы

Аффилиация

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