Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore(algebra/order/group/basic): Improve lemma names #16970

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - chore(algebra/order/group/basic): Improve lemma names #16970

wants to merge 7 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Oct 14, 2022 •
edited
Loading

Rename

  • div_le'' → div_le_comm
  • le_div'' → le_div_comm
  • sub_le → sub_le_comm
  • le_sub → le_sub_comm
  • div_lt'' → div_lt_comm
  • lt_div'' → lt_div_comm
  • sub_lt → sub_lt_comm
  • lt_sub → lt_sub_comm

Open in Gitpod

@YaelDillies YaelDillies requested review from a team as code owners October 14, 2022 07:02
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-order Order hierarchy labels Oct 14, 2022
@fpvandoorn
Copy link
Member

fpvandoorn commented Oct 14, 2022 •
edited
Loading

I think I like swap (EDIT: or rev?) better than comm, but maybe I'm bikeshedding...

@YaelDillies
Copy link
Collaborator Author

It's already used in similar lemmas, like le_compl_comm

@fpvandoorn
Copy link
Member

fpvandoorn commented Oct 14, 2022 •
edited
Loading

I think rev is most common, as in mul_inv_rev, ideal.mul_mem_mul_rev, one_div_mul_one_div_rev, but I can live with _comm.

@YaelDillies YaelDillies requested a review from a team as a code owner October 15, 2022 08:29
@YaelDillies
Copy link
Collaborator Author

Those are precisely not commutativity lemmas however. They are antidistributivity lemmas instead.

@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 1, 2022
bors bot pushed a commit that referenced this pull request Nov 1, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
de03f54 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 1, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 1, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
e479d52 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 1, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 1, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
5563d93 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 1, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 1, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
bf9a105 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 1, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 1, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
731daed 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 1, 2022

Build failed:

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Nov 2, 2022
@fpvandoorn
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Nov 2, 2022

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 2, 2022
@YaelDillies
Copy link
Collaborator Author

Let's try again

bors merge

bors bot pushed a commit that referenced this pull request Nov 3, 2022
@YaelDillies
chore(algebra/order/group/basic): Improve lemma names (#16970)
402f898 
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
@bors
Copy link

bors bot commented Nov 3, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/order/group/basic): Improve lemma names [Merged by Bors] - chore(algebra/order/group/basic): Improve lemma names Nov 3, 2022
@bors bors bot closed this Nov 3, 2022
@bors bors bot deleted the div_le_comm branch November 3, 2022 11:15
@eric-wieser eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Nov 5, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. hacktoberfest-accepted Without this label hacktoberfest is scared off by bors t-order Order hierarchy
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@YaelDillies @fpvandoorn @jcommelin @eric-wieser