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

add variations of nat.mod_add_div #1534

Closed
semorrison opened this issue Oct 9, 2019 · 0 comments
Closed

add variations of nat.mod_add_div #1534

semorrison opened this issue Oct 9, 2019 · 0 comments
Labels
help-wanted The author needs attention to resolve issues

Comments

@semorrison
Copy link
Collaborator

semorrison commented Oct 9, 2019 •
edited
Loading

We have

lemma mod_add_div (m k : ℕ) : m % k + k * (m / k) = m

but it's hard to guess which variant to use. (And, e.g. euclidean_domain provides a different one!)

Let's add at least

lemma div_add_mod (m k : ℕ) : k * (m / k) + m % k = m

and possibly also

lemma mod_add_div' (m k : ℕ) : m % k + (m / k) * k = m
lemma div_add_mod' (m k : ℕ) : (m / k) * k + m % k = m

(with better names?)

Possibly also add all the variations to euclidean_domain?
@robertylewis robertylewis added the help-wanted The author needs attention to resolve issues label Oct 16, 2019
@Julian-Kuelshammer Julian-Kuelshammer mentioned this issue Jan 25, 2021
Closed
bors bot pushed a commit that referenced this issue Jan 27, 2021
@Julian-Kuelshammer
feat(algebra/euclidean_domain): Unify occurences of div_add_mod and m…
21e9d42 
…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>
@Julian-Kuelshammer Julian-Kuelshammer mentioned this issue Jan 29, 2021
Closed
bors bot pushed a commit that referenced this issue Feb 1, 2021
@Julian-Kuelshammer
chore(*) add mod_add_div' and div_add_mod' and golf proofs (#5962)
cbd88d6 
Resolves issue #1534.

Name of nat.mod_add_div shouldn't be changed as this is in core. Better name suggestions for mod_add_div' and div_add_mod' welcome.



Co-authored-by: Julian <kuelsha@mathematik.uni-stuttgart.de>
b-mehta pushed a commit that referenced this issue Apr 2, 2021
@Julian-Kuelshammer @b-mehta
feat(algebra/euclidean_domain): Unify occurences of div_add_mod and m…
e4076d4 
…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>
b-mehta pushed a commit that referenced this issue Apr 2, 2021
@Julian-Kuelshammer @b-mehta
chore(*) add mod_add_div' and div_add_mod' and golf proofs (#5962)
16ff58d 
Resolves issue #1534.

Name of nat.mod_add_div shouldn't be changed as this is in core. Better name suggestions for mod_add_div' and div_add_mod' welcome.



Co-authored-by: Julian <kuelsha@mathematik.uni-stuttgart.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
help-wanted The author needs attention to resolve issues
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@semorrison @robertylewis @Julian-Kuelshammer