Theorem Real.self_sub_one_le_mul_log

Modification history

2026-04-28 23:23

Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

feat(Analysis/SpecialFunctions/Log): Extends log_mul_self_StrictMonoOn (#37717) …

Added Real.self_sub_one_le_mul_log View on Github →