-
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(field_theory/ratfunc): The numerator and denominator of a rational function are coprime #18652
Conversation
…al function are coprime
|
||
lemma gcd_ne_zero_of_left (p q : R) (hp : p ≠ 0) : | ||
gcd_monoid.gcd p q ≠ 0 := | ||
lemma gcd_ne_zero_of_left (hp : p ≠ 0) : gcd_monoid.gcd p q ≠ 0 := |
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.
Why did you make q
implicit here?
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.
This matches the two lemmas right under.
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.
I'd argue the change should be in the other direction (or declared out of scope and not made at all)
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.
Well, I can keep q
explicit if you insist. But this lemma is only used inside this file, and never with explicit arguments.
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.
Let's either keep q
explicit or not touch these lemmas at all.
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.
I think it's fine to have these implicit.
bors merge
@@ -84,6 +84,9 @@ begin | |||
rw [mul_div_cancel_left _ hz, mul_left_comm, mul_div_cancel_left _ hz] | |||
end | |||
|
|||
protected lemma mul_div_cancel' (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a := |
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.
Is there a reason this is primed but mul_div_cancel_left
is not?
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.
This corresponds to mul_div_cancel'
.
…al function are coprime (#18652) Also make more arguments to `gcd_ne_zero_of_left`/`gcd_ne_zero_of_right` implicit. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
#5136) Match leanprover-community/mathlib#18652 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
#5136) Match leanprover-community/mathlib#18652 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
#5136) Match leanprover-community/mathlib#18652 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
#5136) Match leanprover-community/mathlib#18652 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
#5136) Match leanprover-community/mathlib#18652 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Also make more arguments to
gcd_ne_zero_of_left
/gcd_ne_zero_of_right
implicit.Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com