arithGeom_zero_eq_mul_div

Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

← MathLib Explorer

English

For a ≠ 1, arithGeom a b 0 n = b (a^n - 1)/(a - 1).

Русский

Для a ≠ 1: arithGeom(a,b,0,n) = b (a^n - 1)/(a - 1).

LaTeX

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

Lean4

theorem arithGeom_zero_eq_mul_div (ha : a ≠ 1) (n : ℕ) : arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1) := by
  rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg, neg_div, neg_neg]

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

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

Разделы

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

Аффилиация

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