arithGeom_eq_add_sum — Mathlib

English

For all CommSemiring R, arithGeom a b u0 n = a^n u0 + b ∑_{k=0}^{n-1} a^k.

Русский

Для кольца, являющегося коммутативным полем без нуля, имеем явное выражение: arithGeom(a,b,u0,n) = a^n u0 + b ∑_{k=0}^{n-1} a^k.

LaTeX

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

Lean4

theorem arithGeom_eq_add_sum [CommSemiring R] (n : ℕ) :
    arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one, Finset.mul_sum,
      Finset.mul_sum]
    congr with k
    ring

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