Theorem ENNReal.log_zero

Modification history

2026-08-11 00:21
Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
chore: bump toolchain to v4.34.0-rc1 (#42619)
Modified ENNReal.log_zeroView on Github →
2024-07-12 14:35
Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
feat(SpecialFunctions/Log): Add extended exp (#14107) …
Modified ENNReal.log_zeroView on Github →
2024-06-23 16:19
Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean
feat(SpecialFunctions/Log): add extended nonnegative real logarithm (#14018) …
Added ENNReal.log_zeroView on Github →