Theorem Real.exp_lt_exp_of_lt

Modification history

2026-05-17 20:27
Mathlib/Analysis/Complex/Exponential.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted Real.exp_lt_exp_of_ltView on Github →
2023-07-18 02:54
Mathlib/Data/Complex/Exponential.lean
chore: `gcongr` attributes for `exp` (#5968)
Added Real.exp_lt_exp_of_ltView on Github →