Theorems · Theorem · special functions

ordinaryHypergeometricSeries_eq_zero_iff

∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  (a b c : 𝕂) (n : ℕ), ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

An iff variation on ordinaryHypergeometricSeries_eq_zero_of_nonpos_int for [RCLike 𝕂].

Defined in

Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedDivisionRingNormedAlgebra