Theorem EReal.exp_lt_exp

Modification history

2025-10-27 16:35
Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Modified EReal.exp_lt_expView on Github →
2025-05-23 23:59
Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
chore(*): use gcongr (#24720) …
Added EReal.exp_lt_expView on Github →