Theorem Real.mul_log_strictMonoOn

Modification history

2026-04-28 23:23

Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

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

Added Real.mul_log_strictMonoOn View on Github →