-
Notifications
You must be signed in to change notification settings - Fork 298
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
feat(data/int/gcd) extended gcd to integers #218
Conversation
data/int/basic.lean
Outdated
@@ -423,7 +423,7 @@ theorem mod_eq_zero_of_dvd : ∀ {a b : ℤ}, a ∣ b → b % a = 0 | |||
theorem dvd_iff_mod_eq_zero (a b : ℤ) : a ∣ b ↔ b % a = 0 := | |||
⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ | |||
|
|||
theorem nat_abs_dvd {a b : ℤ} : (a.nat_abs : ℤ) ∣ b ↔ a ∣ b := | |||
theorem nat_abs_dvd {a b : ℤ} : (a.nat_abs : ℤ) ∣ b ↔ a ∣ b := |
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.
You added a space at the end of this line.
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 for letting me know, the extra spaces are now removed.
I don't think this is the way we want to go. The way to go is to introduce a GCD (semi-)domain. |
@gml16 do you want to work on GCD (semi-) domains? |
Sure if it's useful feel free to pull the content :) |
Resurrected by @johoelzl. The original commit was not available anymore.
Resurrected by @johoelzl. The original commit was not available anymore.
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list