Theorems · Theorem · special functions

ordinaryHypergeometric_sum_eq

∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (x : 𝔸),
  (ordinaryHypergeometricSeries 𝔸 a b c).sum x =
    ∑' (n : ℕ),
      ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
        x ^ n

Defined in

Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Cited by

1 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebraTopologicalSpaceIsTopologicalRing