Theorem Real.le_inv_mul_exp

Modification history

2025-01-19 09:13
Mathlib/Data/Complex/Exponential.lean
feat: describe the interval of reals `t` where `exp (t * X)` is integrable (#20418) …
Added Real.le_inv_mul_expView on Github →