Theorem Real.mul_log_pos

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