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: a/c ≡ b/c mod m/c → a ≡ b mod m
#3259
Conversation
Mathlib/Algebra/Group/Basic.lean
Outdated
@@ -496,7 +496,7 @@ theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp | |||
#align inv_mul' inv_mul' | |||
#align neg_add' neg_add' | |||
|
|||
@[to_additive] | |||
@[to_additive (attr := simp)] |
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 is tagged simp in mathlib. As there is no porting note, I assume dropping the simp was an error.
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.
If the simp is there in mathlib4 it gives linter errors; removing that simp makes everything check out.
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 you need to have simp
only on the multiplicative version?
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.
It doesn't make "everything check out" since the proof of my new lemma broke because it was missing. However, it's easy to work around it and potentially non trivial to solve, so I'm leaving a porting note and outsourcing the problem to #3309.
This doesn't have anything to do with additive vs multiplicative stuff. At this level, both worlds have the same simp lemmas.
502d29e
to
8e751c5
Compare
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.
Please clarify the porting comment about swap
, otherwise LGTM!
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...): |
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...):
|
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors r- |
Canceled. |
8febd78
to
8aefd69
Compare
Should be good this time. bors merge |
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
a/c ≡ b/c mod m/c → a ≡ b mod m
a/c ≡ b/c mod m/c → a ≡ b mod m
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666. * [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.gcd`@`d4f69d96f3532729da8ebb763f4bc26fcf640f06`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/gcd?range=d4f69d96f3532729da8ebb763f4bc26fcf640f06..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.nat.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.int.modeq`@`2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/modeq?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`algebra.char_p.basic`@`ceb887ddf3344dab425292e497fa2af91498437c`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/char_p/basic?range=ceb887ddf3344dab425292e497fa2af91498437c..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) * [`data.zmod.basic`@`297619ec79dedf23525458b6bf5bf35c736fd2b8`..`47a1a73351de8dd6c8d3d32b569c8e434b03ca47`](https://leanprover-community.github.io/mathlib-port-status/file/data/zmod/basic?range=297619ec79dedf23525458b6bf5bf35c736fd2b8..47a1a73351de8dd6c8d3d32b569c8e434b03ca47) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community/mathlib#18119, leanprover-community/mathlib#18666.
algebra.ring.divisibility
@f1a2caaf51ef593799107fe9a8d5e411599f3996
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
data.nat.order.lemmas
@2258b40dacd2942571c8ce136215350c702dc78f
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
data.int.gcd
@d4f69d96f3532729da8ebb763f4bc26fcf640f06
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
data.nat.modeq
@2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
data.int.modeq
@2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
algebra.char_p.basic
@ceb887ddf3344dab425292e497fa2af91498437c
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47
data.zmod.basic
@297619ec79dedf23525458b6bf5bf35c736fd2b8
..47a1a73351de8dd6c8d3d32b569c8e434b03ca47