Theorem Complex.mul_regularizedHGFunCoeff_of_mem_right

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