Commit 2025-10-29 09:13 f531e600

View on Github →

feat: elementary lemmas aiding computations with log⁺, Mark II (#30729) Add several elementary lemmas aiding computations with log⁺. Improve the docstrings a little.

Estimated changes

modified theorem Real.posLog_nat_mul
modified theorem Real.posLog_norm_add_le
added theorem Real.posLog_one
added theorem Real.posLog_pow
added theorem Real.posLog_zero