Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 17:34 3103a89b

View on Github →

feat(analysis/special_functions/exp): a lemma about exp (f x) =O[l] const _ _ (#14524)

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

added theorem asymptotics.is_O_const_left_iff_pos_le_norm

Modified src/analysis/special_functions/exp.lean

added theorem real.is_O_one_exp_comp