-
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/euclidean_domain): Unify occurences of div_add_mod and mod_add_div #5884
Conversation
…n to unify with nat
…th euclidean domain
…ith euclidean domain
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
… for int, but not for pnat because of some coercion
Are |
They are not, see the issue. Do you have a suggestion for a better name than just 'priming' everything? |
Add in the word
|
I suggest to leave the PR like that and do the potential other two versions, potential renaming, and golfing of proofs for other PRs as it is always very slow to edit such basic files as nat and int. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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 🎉
bors merge
…od_add_div (#5884) Adding the corresponding commutative version at several places (euclidean domain, nat, pnat, int) whenever there is the other version. In subsequent PRs other proofs in the library which now use some version of `add_comm, exact div_add_mod` or `add_comm, exact mod_add_div` should be golfed. Trying to address issue #1534 Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…od_add_div (#5884) Adding the corresponding commutative version at several places (euclidean domain, nat, pnat, int) whenever there is the other version. In subsequent PRs other proofs in the library which now use some version of `add_comm, exact div_add_mod` or `add_comm, exact mod_add_div` should be golfed. Trying to address issue #1534 Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Adding the corresponding commutative version at several places (euclidean domain, nat, pnat, int) whenever there is the other version.
In subsequent PRs other proofs in the library which now use some version of
add_comm, exact div_add_mod
oradd_comm, exact mod_add_div
should be golfed.Trying to address issue #1534