-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/nat/modeq): add modeq and dvd lemmas from Apostol Chapter 5 #11787
Conversation
Are we sure these theorems or anything similar to them aren't in mathlib already? They all seem pretty basic. |
They do, but I couldn't resolve them with |
@vihdzp I think I've addressed all your comments now. Thanks very much for your helpful suggestions, especially the suggested lemma names. |
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.
As far as I can tell, these are new lemmas, thanks.
Thanks @stuart-presnell for the PR and @vihdzp for the detailed review! bors merge |
…#11787) Various lemmas about `modeq` from Chapter 5 of Apostol (1976) Introduction to Analytic Number Theory: * `mul_left_iff` and `mul_right_iff`: Apostol, Theorem 5.3 * `dvd_iff_of_modeq_of_dvd`: Apostol, Theorem 5.5 * `gcd_eq_of_modeq`: Apostol, Theorem 5.6 * `eq_of_modeq_of_abs_lt`: Apostol, Theorem 5.7 * `modeq_cancel_left_div_gcd`: Apostol, Theorem 5.4; plus other cancellation lemmas following from this.
Pull request successfully merged into master. Build succeeded: |
Various lemmas about
modeq
from Chapter 5 of Apostol (1976) Introduction to Analytic Number Theory:mul_left_iff
andmul_right_iff
: Apostol, Theorem 5.3dvd_iff_of_modeq_of_dvd
: Apostol, Theorem 5.5gcd_eq_of_modeq
: Apostol, Theorem 5.6eq_of_modeq_of_abs_lt
: Apostol, Theorem 5.7modeq_cancel_left_div_gcd
: Apostol, Theorem 5.4; plus other cancellation lemmas following from this.