Theorems · Definition · special functions
Complex.regularizedHGFunSeries
Multiset ℂ → Multiset ℂ → FormalMultilinearSeries ℂ ℂ ℂ
The regularized hypergeometric series.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- Multisetstatement and proof · cited by 2,627
- FormalMultilinearSeriesstatement · cited by 615
- FormalMultilinearSeries.ofScalarsproof · cited by 68
- Complex.regularizedHGFunCoeffproof · cited by 10
Cited by10
Results whose statement or proof uses this declaration.
- Complex.regularizedGaussHGFunSeriesproof · cited by 9
- Complex.radius_regularizedHGFunSeries_eq_top_of_finitestatement and proof · cited by 4
- Complex.regularizedHGFunSeries_coeffstatement · cited by 2
- Complex.radius_regularizedHGFunSeries_eq_onestatement · cited by 1
- Complex.radius_regularizedHGFunSeries_ge_onestatement · cited by 1
- Complex.regularizedGaussHGFunSeries_symmproof · cited by 1
- Complex.regularizedHGFunproof · cited by 1
- Complex.regularizedHGFunSeries_zero_zerostatement · cited by 1
- Complex.radius_regularizedHGFunSeries_eq_topstatement · cited by 0
- Complex.regularizedHGFunSeries_eq_zerostatement · cited by 0