[Merged by Bors] - feat(analysis/special_functions/pow): Added lemmas for rpow of neg exponent

[benjamindavidson]

I noticed that the library was missing some lemmas regarding the bounds of rpow of a negative exponent so I added them. I cleaned up the other similar preexisting lemmas for consistency. I then repeated the process for nnreal lemmas.

---

I chose to use ' in the naming of the lemmas that deal with a negative exponent.

[ChrisHughes24]

Just some name changes, there are a few lemmas that need descriptive names that I didn't ment

[benjamindavidson]

Just some name changes, there are a few lemmas that need descriptive names that I didn't ment

I was mimicking the names of the preexisting lemmas. But I will gladly change them to match the pattern that you've suggested if that is preferable.

[semorrison]

@benjamindavidson it's helpful in the review process if you can click "resolve conversation" on items that have uncontroversially been solved, so new reviewers coming to the PR don't have to analyse what has and hasn't been done.

[benjamindavidson]

@benjamindavidson it's helpful in the review process if you can click "resolve conversation" on items that have uncontroversially been solved, so new reviewers coming to the PR don't have to analyse what has and hasn't been done.

Noted! Thanks for the advice and please do excuse my inexperience.

[robertylewis]

In a way this is the hardest kind of PR to review! All looks good to me. But I could stare at these different permutations for an hour and still miss one with the wrong name. If someone else agrees with me that these look right let's merge.

[Vierkantor]

Looks good to me.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests