Commit 2025-10-31 17:31 b58c711e

View on Github →

chore(Analysis/SpecialFunctions/Log/PosLog): uniformize variable names (#31084) As a follow-up to PR #30641, uniformize the variable names in Analysis/SpecialFunctions/Log/PosLog.lean, for brevity and improved readability.

Estimated changes

modified theorem Real.posLog_add
modified theorem Real.posLog_def
modified theorem Real.posLog_eq_log
modified theorem Real.posLog_eq_log_max_one
modified theorem Real.posLog_le_posLog
modified theorem Real.posLog_mul
modified theorem Real.posLog_nat_mul
modified theorem Real.posLog_nonneg
modified theorem Real.posLog_sub_posLog_inv