Theorems · Theorem · special functions

ordinaryHypergeometricSeries_apply_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 : 𝔸) (n : ℕ),
  ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 => x) =
    ((↑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 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebraTopologicalSpaceIsTopologicalRing