-
Notifications
You must be signed in to change notification settings - Fork 299
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_group): -abs a ≤ a
#7839
Conversation
We don't normally have lemmas that are conjunctions of other lemmas (unless proving the conjunction is easier for some reason than proving the parts, in which case it's usually an auxiliary lemma and the parts are separated immediately after). I would just keep the first lemma. |
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.
bors r+
Thanks!
-abs a ≤ a ≤ abs a
-abs a ≤ a
The failing CI run looks like it's a CDN issue unrelated to this PR. It's still quite likely bors will trip up on the same thing, but there's not much we can do about that anyway. |
This PR was included in a batch that timed out, it will be automatically retried |
bors r- |
Canceled. |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
-abs a ≤ a
-abs a ≤ a
No description provided.