Theorem Complex.regularizedHGFun_zero_singleton_eq_mul_add_mul

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.regularizedHGFun_zero_singleton_eq_mul_add_mulView on Github →