Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 21:24 be88ceca

View on Github →

feat(analysis/exponential): added inequality lemmas

Estimated changes

Modified src/analysis/exponential.lean

added theorem real.log_le_log

added theorem real.mul_rpow

added theorem real.one_le_rpow

modified theorem real.pow_nat_rpow_nat_inv

added theorem real.rpow_le_rpow

Modified src/data/complex/exponential.lean

modified theorem real.exp_le_exp