Theorem Real.negMulLog_le_one_sub_self

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.negMulLog_le_one_sub_self View on Github →