Theorem Real.not_DifferentiableAt_log_mul_zero

Modification history

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