Theorem Real.deriv_mul_log_zero

Modification history

2024-08-10 08:13
Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
feat: Generalize statements about deriv of MulLog (#14594) …
Added Real.deriv_mul_log_zeroView on Github →