Theorem Real.exp_le_exp_of_le

Modification history

2023-07-18 02:54
Mathlib/Data/Complex/Exponential.lean
chore: `gcongr` attributes for `exp` (#5968)
Added Real.exp_le_exp_of_leView on Github →