arithGeom_same_eq_mul_div'

Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

URI: https://scilib.ai/kg/mathlib#arithGeom_same_eq_mul_div'

← MathLib Explorer

English

For a ≠ 1, arithGeom a b b n = b (1 - a^{n+1})/(1 - a).

Русский

При a ≠ 1 имеем arithGeom(a,b,b,n) = b (1 - a^{n+1})/(1 - a).

LaTeX

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

Lean4

theorem arithGeom_same_eq_mul_div' (ha : a ≠ 1) (n : ℕ) : arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a) :=
  by
  rw [arithGeom_eq ha n]
  have : 1 - a ≠ 0 := sub_ne_zero.mpr ha.symm
  field_simp
  ring

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

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

Разделы

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

Аффилиация

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