New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/ordered_field): a few monotonicity results for powers #8022
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One name seems to be a bit off.
bors d+
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks, Johan! I updated the name with your suggestion and will wait for CI to finish before merging! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the new lemmas, they look good other than the names
bors e+ |
damiano, you used the wrong letter :b |
bors r+ |
Eric, thanks! I used my phone and |
Build failed: |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
This PR proves the monotonicity (strict and non-strict) of
n → 1 / a ^ n
, for a fixeda < 1
in a linearly ordered field. These are lemmas extracted from PR #8001: I moved them to a separate PR after the discussion there.