arithGeom_zero_eq_sum

Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

English

If the starting value is 0, then arithGeom a b 0 n = b ∑_{k=0}^{n-1} a^k.

Русский

Если начальное значение равно 0, то arithGeom(a,b,0,n) = b ∑_{k=0}^{n-1} a^k.

LaTeX

$$$\mathrm{arithGeom}(a,b,0,n) = b \displaystyle\sum_{k=0}^{n-1} a^k$$$

Lean4

theorem arithGeom_zero_eq_sum [CommSemiring R] (n : ℕ) : arithGeom a b 0 n = b * ∑ k ∈ Finset.range n, a ^ k := by
  simp [arithGeom_eq_add_sum]

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

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

Разделы

Аффилиация

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