[Merged by Bors] - feat(data/nat/modeq): Generalised version of the Chinese remainder theorem #5683
Conversation
alexjbest
added
the
awaiting-review
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bryangingechen
changed the title
github-actions
bot
added
the
merge-conflict
jcommelin
added
the
awaiting-author
github-actions
bot
removed
the
merge-conflict
alexjbest
removed
the
awaiting-author
| @@ -736,6 +739,13 @@ theorem neg_div_of_dvd : ∀ {a b : ℤ} (H : b ∣ a), -a / b = -(a / b) | |||
| | ._ b ⟨c, rfl⟩ := if bz : b = 0 then by simp [bz] else | |||
| by rw [neg_mul_eq_mul_neg, int.mul_div_cancel_left _ bz, int.mul_div_cancel_left _ bz] | |||
|
|
|||
| lemma sub_div_of_dvd {a b c : ℤ} (hcb : c ∣ b) : (a - b) / c = a / c - b / c := | |||
There was a problem hiding this comment.
Do you mind renaming this to sub_div_of_dvd_right and adding the left version?
There was a problem hiding this comment.
At least the obvious left version isn't true!
lemma sub_div_of_dvd {a b c : ℤ} (hcb : c ∣ a) : (a - b) / c = a / c - b / c := by slim_check
===================
Found problems!
a := 0
b := 1
c := 2
issue: -1 = 0 does not hold
(5 shrinks)I guess the version
lemma sub_div_of_dvd_sub {a b c : ℤ} (hcab : c ∣ (a - b)) : (a - b) / c = a / c - b / c :=
by rw [eq_sub_iff_add_eq, ← int.add_div_of_dvd_left hcab, sub_add_cancel]is actually true, not sure how useful that is though?
There was a problem hiding this comment.
Oh, whoops. OK, we can just leave this as is then.
There was a problem hiding this comment.
Yeah I had exactly the same thought a few days ago and spent 5 mins trying to prove it 😬 I'll add this other version to the PR though, and maybe an add version of that too, why not lol
github-actions
bot
added
ready-to-merge
…eorem (#5683) That allows the moduli to not be coprime, assuming the necessary condition. Old crt is now in terms of this one
|
bors r- I think Alex still wanted to add a few more helper lemmas. @alexjbest Feel free to merge when you're happy! |
|
✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Canceled. |
|
Thanks, in the end the add version wasn't true either :) so just one more here. bors r+ |
…eorem (#5683) That allows the moduli to not be coprime, assuming the necessary condition. Old crt is now in terms of this one
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
That allows the moduli to not be coprime, assuming the necessary condition. Old crt is now in terms of this one