Theorem ENNReal.log_pow

Modification history

2024-07-14 02:03
Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
feat(SpecialFunctions.Log.ENNRealLog): remove a coercion in log_pow (#14714) …
Modified ENNReal.log_powView 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_powView on Github →