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] - feat(algebra/field/basic): div_neg_self, neg_div_self #11438

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(algebra/field/basic): div_neg_self, neg_div_self #11438

wants to merge 1 commit into from

Conversation

jsm28
Copy link
Collaborator

@jsm28 jsm28 commented Jan 14, 2022

I think these two lemmas are useful as simp lemmas, but they don't
seem to be there already.

Open in Gitpod

@jsm28
feat(algebra/field/basic): div_neg_self, neg_div_self
c742654 
I think these two lemmas are useful as `simp` lemmas, but they don't
seem to be there already.
@jsm28 jsm28 added the awaiting-review The author would like community review of the PR label Jan 14, 2022
@jcommelin
Copy link
Member

Should they also be taught to field_simp?

@jsm28
Copy link
Collaborator Author

jsm28 commented Jan 14, 2022

by field_simp [h] can prove both lemmas (when the field_simp tactic is visible, which it isn't at this point). So I'm not sure it's useful to mark them as @[field_simps].

@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 Jan 14, 2022
bors bot pushed a commit that referenced this pull request Jan 14, 2022
@jsm28
feat(algebra/field/basic): div_neg_self, neg_div_self (#11438)
22a9f2e 
I think these two lemmas are useful as `simp` lemmas, but they don't
seem to be there already.
@bors
Copy link

bors bot commented Jan 14, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/field/basic): div_neg_self, neg_div_self [Merged by Bors] - feat(algebra/field/basic): div_neg_self, neg_div_self Jan 14, 2022
@bors bors bot closed this Jan 14, 2022
@bors bors bot deleted the jsm28/div_neg_self branch January 14, 2022 16:38
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
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@jsm28 @jcommelin