Theorem Real.posLog_norm_sum_le

Modification history

2025-10-29 09:13
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: elementary lemmas aiding computations with `log⁺`, Mark II (#30729) …
Added Real.posLog_norm_sum_leView on Github →