Commit 2022-09-29 01:02 e63a4d5e

View on Github →

feat(analysis/special_functions/pow): sqrt and inequalities (#16515) This PR proves a few lemmas about real.sqrt and real.rpow as well as inequality lemmas for negative powers.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem real.le_rpow_inv_iff_of_neg

added theorem real.lt_rpow_inv_iff_of_neg

added theorem real.rpow_div_two_eq_sqrt

added theorem real.rpow_inv_le_iff_of_neg

added theorem real.rpow_inv_lt_iff_of_neg