arithGeom_eq — Mathlib

English

For a field R and a ≠ 1, arithGeom a b u0 n = a^n (u0 - b/(1-a)) + b/(1-a).

Русский

Для кольца поля и при a ≠ 1 имеем arithGeom(a,b,u0,n) = a^n (u0 - b/(1-a)) + b/(1-a).

LaTeX

$$$\mathrm{arithGeom}(a,b,u_0,n) = a^n \bigl(u_0 - \frac{b}{1-a}\bigr) + \frac{b}{1-a}$$$

Lean4

theorem arithGeom_eq (ha : a ≠ 1) (n : ℕ) : arithGeom a b u₀ n = a ^ n * (u₀ - (b / (1 - a))) + b / (1 - a) := by
  induction n with
  | zero => simp
  | succ n hn => unfold arithGeom; grind

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