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] - refactor(algebra/order/{smul,module}): Turn lemmas around #16696

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - refactor(algebra/order/{smul,module}): Turn lemmas around #16696

wants to merge 3 commits into from

Conversation

YaelDillies
Copy link
Collaborator

Match the mul lemmas by having the ⁻¹ on the LHS in inv_smul_le_iff, inv_smul_lt_iff, etc... Also generalize for free to ordered_add_comm_monoid.

Open in Gitpod

@YaelDillies YaelDillies added t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy WIP Work in progress labels Sep 29, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed WIP Work in progress labels Sep 29, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 30, 2022
jcommelin
jcommelin approved these changes Sep 30, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Sep 30, 2022
bors bot pushed a commit that referenced this pull request Sep 30, 2022
@YaelDillies
refactor(algebra/order/{smul,module}): Turn lemmas around (#16696)
64ad902 
Match the `mul` lemmas by having the `⁻¹` on the LHS in `inv_smul_le_iff`, `inv_smul_lt_iff`, etc... Also generalize for free to `ordered_add_comm_monoid`.
@bors
Copy link

bors bot commented Sep 30, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(algebra/order/{smul,module}): Turn lemmas around [Merged by Bors] - refactor(algebra/order/{smul,module}): Turn lemmas around Sep 30, 2022
@bors bors bot closed this Sep 30, 2022
@bors bors bot deleted the inv_smul_le_iff branch September 30, 2022 16:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @jcommelin @leanprover-community-bot-assistant