ordinaryHypergeometricSeries_apply_zero

English

Equality of the tsum form with the explicit coefficient form for the hypergeometric series.

Русский

Эквивалентность формы через tsum и явной формы коэффициентов для гипергеометрической серии.

LaTeX

$$$( ordinaryHypergeometricSeries( a,b,c) ).sum x = \\sum_{n\\ge0} coeff_n x^n$$$

Lean4

theorem ordinaryHypergeometricSeries_apply_zero (n : ℕ) :
    ordinaryHypergeometricSeries 𝔸 a b c n (fun _ => 0) = Pi.single (M := fun _ => 𝔸) 0 1 n :=
  by
  rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]
  cases n <;> simp

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