Theorem Real.mul_log_strictAntiOn

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_strictAntiOnView on Github →