Theorem ProbabilityTheory.hasDerivAt_neg_exp_mul_exp

Modification history

2023-11-21 21:57
Mathlib/Probability/Distributions/Exponential.lean
feat: Real Exponential Distribution (#8253) …
Added ProbabilityTheory.hasDerivAt_neg_exp_mul_expView on Github →