Theorem Real.log_mul_self_monotoneOn

Modification history

2026-10-16 07:34
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
chore: remove declarations deprecated between 2026-04-01 and 2026-04-15 (#44903) …
Deleted Real.log_mul_self_monotoneOnView on Github →
2023-05-20 16:09
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
feat: port Analysis.SpecialFunctions.Log.Monotone (#4144)
Added Real.log_mul_self_monotoneOnView on Github →