Theorem Complex.summable_pow_mul_regularizedHGFunCoeff_zero

Modification history

2026-10-20 13:30
Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean
feat(Analysis/SpecialFunctions): the recurrence relation of bessel function J (#43853) …
Added Complex.summable_pow_mul_regularizedHGFunCoeff_zeroView on Github →