Theorems · Definition · special functions

ordinaryHypergeometric

{𝕂 : Type u_1} →
  {𝔸 : Type u_2} →
    [inst : Field 𝕂] →
      [inst_1 : Ring 𝔸] → [Algebra 𝕂 𝔸] → [inst : TopologicalSpace 𝔸] → [IsTopologicalRing 𝔸] → 𝕂 → 𝕂 → 𝕂 → 𝔸 → 𝔸

ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸, denoted ₂F₁, is the ordinary hypergeometric map, defined as the sum of the FormalMultilinearSeries ordinaryHypergeometricSeries 𝔸 a b c. Note that this takes the junk value 0 outside the radius of convergence.

Defined in

Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraTopologicalSpaceIsTopologicalRing