[Merged by Bors] - feat(field_theory/ratfunc): The numerator and denominator of a rational function are coprime #18652
Conversation
…al function are coprime
YaelDillies
added
awaiting-review
|
|
||
| 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.
Why did you make q implicit here?
There was a problem hiding this comment.
This matches the two lemmas right under.
There was a problem hiding this comment.
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.
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.
Let's either keep q explicit or not touch these lemmas at all.
There was a problem hiding this comment.
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.
Is there a reason this is primed but mul_div_cancel_left is not?
There was a problem hiding this comment.
This corresponds to mul_div_cancel'.
semorrison
added
the
modifies-synchronized-file
…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. |
bors
bot
changed the title
#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_rightimplicit.Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com