Theorem Complex.two_mul_self_mul_besselJ

Modification history

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