Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 09:38 4d5d7708

View on Github →

feat(data/complex/exponential): Add lemma add_one_le_exp (#10358) This PR resolves https://github.com/leanprover-community/mathlib/blob/master/src/data/complex/exponential.lean#L1140

Estimated changes

Modified src/analysis/special_functions/exp.lean

Modified src/data/complex/exponential.lean

added theorem real.add_one_le_exp

added theorem real.add_one_le_exp_of_nonpos

added theorem real.exp_bound'

added theorem real.exp_bound_div_one_sub_of_interval

added theorem real.exp_bound_div_one_sub_of_interval_approx

added theorem real.one_sub_le_exp_minus_of_pos