Theorem Real.log_mul_self_monotoneOn

Modification history

2023-05-20 16:09

Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

feat: port Analysis.SpecialFunctions.Log.Monotone (#4144)

Added Real.log_mul_self_monotoneOn View on Github →