Commit 2023-07-18 02:54 6dbfca47

View on Github →

chore: gcongr attributes for exp (#5968)

Estimated changes

Modified Mathlib/Data/Complex/Exponential.lean

added theorem Real.exp_le_exp_of_le

added theorem Real.exp_lt_exp_of_lt