Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(algebra/divisibility/basic): Dot notation aliases #18698

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat(algebra/divisibility/basic): Dot notation aliases #18698

wants to merge 14 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Mar 29, 2023 •
edited

A few convenience shortcuts for dvd along with some simple nat lemmas. Also

  • Drop neg_dvd_of_dvd/dvd_of_neg_dvd/dvd_neg_of_dvd/dvd_of_dvd_neg in favor of the aforementioned shortcuts.
  • Remove explicit arguments to dvd_neg/neg_dvd.
  • Drop int.of_nat_dvd_of_dvd_nat_abs/int.dvd_nat_abs_of_of_nat_dvd because they are the two directions of int.coe_nat_dvd_left.
  • Move group_with_zero.to_cancel_monoid_with_zero from algebra.group_with_zero.units.basic back to algebra.group_with_zero.basic. It was erroneously moved during the Great Splits.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Mar 29, 2023
This was referenced Mar 29, 2023
Closed
Closed
@semorrison
Copy link
Collaborator

@YaelDillies, would you mind adding the modifies-synchronized-file label where appropriate? It's very helpful to have this information.

@semorrison semorrison added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 30, 2023
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 31, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 31, 2023
@YaelDillies YaelDillies mentioned this pull request Apr 2, 2023
Closed
1 task
@YaelDillies YaelDillies mentioned this pull request Apr 2, 2023
Closed
3 tasks
@YaelDillies YaelDillies mentioned this pull request Apr 3, 2023
Closed
@YaelDillies YaelDillies requested a review from a team as a code owner April 3, 2023 12:20
@YaelDillies YaelDillies removed the request for review from a team April 3, 2023 12:21
Vierkantor
Vierkantor reviewed Apr 4, 2023
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM otherwise, it's always nice to have more dot notation.

Vierkantor
Vierkantor approved these changes Apr 4, 2023
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice job on the generalization!

bors d+

src/data/nat/order/lemmas.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Apr 4, 2023

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 4, 2023
@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Apr 4, 2023
@YaelDillies
feat(algebra/divisibility/basic): Dot notation aliases (#18698)
980295d 
A few convenience shortcuts for `dvd` along with some simple `nat` lemmas. Also
* Drop `neg_dvd_of_dvd`/`dvd_of_neg_dvd`/`dvd_neg_of_dvd`/`dvd_of_dvd_neg` in favor of the aforementioned shortcuts.
* Remove explicit arguments to `dvd_neg`/`neg_dvd`.
* Drop `int.of_nat_dvd_of_dvd_nat_abs`/`int.dvd_nat_abs_of_of_nat_dvd` because they are the two directions of `int.coe_nat_dvd_left`.
* Move `group_with_zero.to_cancel_monoid_with_zero` from `algebra.group_with_zero.units.basic` back to `algebra.group_with_zero.basic`. It was erroneously moved during the Great Splits.
@bors
Copy link

bors bot commented Apr 4, 2023

Build failed:

@YaelDillies
Copy link
Collaborator Author

I overestimated the diff's abilities 😦

bors merge

bors bot pushed a commit that referenced this pull request Apr 5, 2023
@YaelDillies
feat(algebra/divisibility/basic): Dot notation aliases (#18698)
e8638a0 
A few convenience shortcuts for `dvd` along with some simple `nat` lemmas. Also
* Drop `neg_dvd_of_dvd`/`dvd_of_neg_dvd`/`dvd_neg_of_dvd`/`dvd_of_dvd_neg` in favor of the aforementioned shortcuts.
* Remove explicit arguments to `dvd_neg`/`neg_dvd`.
* Drop `int.of_nat_dvd_of_dvd_nat_abs`/`int.dvd_nat_abs_of_of_nat_dvd` because they are the two directions of `int.coe_nat_dvd_left`.
* Move `group_with_zero.to_cancel_monoid_with_zero` from `algebra.group_with_zero.units.basic` back to `algebra.group_with_zero.basic`. It was erroneously moved during the Great Splits.
@bors
Copy link

bors bot commented Apr 5, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/divisibility/basic): Dot notation aliases [Merged by Bors] - feat(algebra/divisibility/basic): Dot notation aliases Apr 5, 2023
@bors bors bot closed this Apr 5, 2023
@bors bors bot deleted the dvd_of_eq branch April 5, 2023 10:55
This was referenced Apr 6, 2023
Closed
Closed
bors bot pushed a commit that referenced this pull request Apr 10, 2023
@YaelDillies
chore(algebra/group_with_zero/units/basic): Deduplicate instance (#18785
df5e993 
)

`group_with_zero.cancel_monoid_with_zero` was a duplicate of `group_with_zero.to_cancel_monoid_with_zero`.
`comm_group_with_zero.cancel_comm_monoid_with_zero` is renamed to include the usual `to_` prefix.

This should have been done in #18698.
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2023
@YaelDillies @Parcly-Taxel
feat: Dot notation aliases (#3303)
613e4e7 
Match leanprover-community/mathlib#18698 and a bit of leanprover-community/mathlib#18785.

* [`algebra.divisibility.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/divisibility/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.euclidean_domain.basic`@`655994e298904d7e5bbd1e18c95defd7b543eb94`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/euclidean_domain/basic?range=655994e298904d7e5bbd1e18c95defd7b543eb94..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group.units`@`369525b73f229ccd76a6ec0e0e0bf2be57599768`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/units?range=369525b73f229ccd76a6ec0e0e0bf2be57599768..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.units.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`df5e9937a06fdd349fc60106f54b84d47b1434f0`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/units/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..df5e9937a06fdd349fc60106f54b84d47b1434f0)
* [`algebra.order.monoid.canonical.defs`@`de87d5053a9fe5cbde723172c0fb7e27e7436473`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/canonical/defs?range=de87d5053a9fe5cbde723172c0fb7e27e7436473..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.basic`@`e1bccd6e40ae78370f01659715d3c948716e3b7e`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/basic?range=e1bccd6e40ae78370f01659715d3c948716e3b7e..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.pow`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/pow?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.order.basic`@`728baa2f54e6062c5879a3e397ac6bac323e506f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/order/basic?range=728baa2f54e6062c5879a3e397ac6bac323e506f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.gcd.basic`@`a47cda9662ff3925c6df271090b5808adbca5b46`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/gcd/basic?range=a47cda9662ff3925c6df271090b5808adbca5b46..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.basic`@`26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/basic?range=26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`group_theory.perm.cycle.basic`@`92ca63f0fb391a9ca5f22d2409a6080e786d99f7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/perm/cycle/basic?range=92ca63f0fb391a9ca5f22d2409a6080e786d99f7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.divisors`@`f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/divisors?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.pythagorean_triples`@`70fd9563a21e7b963887c9360bd29b2393e6225a`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/pythagorean_triples?range=70fd9563a21e7b963887c9360bd29b2393e6225a..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.zsqrtd.basic`@`7ec294687917cbc5c73620b4414ae9b5dd9ae1b4`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/zsqrtd/basic?range=7ec294687917cbc5c73620b4414ae9b5dd9ae1b4..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`ring_theory.multiplicity`@`ceb887ddf3344dab425292e497fa2af91498437c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/multiplicity?range=ceb887ddf3344dab425292e497fa2af91498437c..e8638a0fcaf73e4500469f368ef9494e495099b3)



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
eric-wieser pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 12, 2023
@YaelDillies @Parcly-Taxel @leanprover-community-bot
feat: Dot notation aliases (#3303)
4fa401f 
Match leanprover-community/mathlib#18698 and a bit of leanprover-community/mathlib#18785.

* [`algebra.divisibility.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/divisibility/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.euclidean_domain.basic`@`655994e298904d7e5bbd1e18c95defd7b543eb94`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/euclidean_domain/basic?range=655994e298904d7e5bbd1e18c95defd7b543eb94..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group.units`@`369525b73f229ccd76a6ec0e0e0bf2be57599768`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/units?range=369525b73f229ccd76a6ec0e0e0bf2be57599768..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.group_with_zero.units.basic`@`70d50ecfd4900dd6d328da39ab7ebd516abe4025`..`df5e9937a06fdd349fc60106f54b84d47b1434f0`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_with_zero/units/basic?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..df5e9937a06fdd349fc60106f54b84d47b1434f0)
* [`algebra.order.monoid.canonical.defs`@`de87d5053a9fe5cbde723172c0fb7e27e7436473`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/canonical/defs?range=de87d5053a9fe5cbde723172c0fb7e27e7436473..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`algebra.ring.divisibility`@`f1a2caaf51ef593799107fe9a8d5e411599f3996`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/divisibility?range=f1a2caaf51ef593799107fe9a8d5e411599f3996..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.basic`@`e1bccd6e40ae78370f01659715d3c948716e3b7e`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/basic?range=e1bccd6e40ae78370f01659715d3c948716e3b7e..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.dvd.pow`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/dvd/pow?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.int.order.basic`@`728baa2f54e6062c5879a3e397ac6bac323e506f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/int/order/basic?range=728baa2f54e6062c5879a3e397ac6bac323e506f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.gcd.basic`@`a47cda9662ff3925c6df271090b5808adbca5b46`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/gcd/basic?range=a47cda9662ff3925c6df271090b5808adbca5b46..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.basic`@`26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/basic?range=26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`data.nat.order.lemmas`@`2258b40dacd2942571c8ce136215350c702dc78f`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/order/lemmas?range=2258b40dacd2942571c8ce136215350c702dc78f..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`group_theory.perm.cycle.basic`@`92ca63f0fb391a9ca5f22d2409a6080e786d99f7`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/perm/cycle/basic?range=92ca63f0fb391a9ca5f22d2409a6080e786d99f7..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.divisors`@`f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/divisors?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.pythagorean_triples`@`70fd9563a21e7b963887c9360bd29b2393e6225a`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/pythagorean_triples?range=70fd9563a21e7b963887c9360bd29b2393e6225a..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`number_theory.zsqrtd.basic`@`7ec294687917cbc5c73620b4414ae9b5dd9ae1b4`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/number_theory/zsqrtd/basic?range=7ec294687917cbc5c73620b4414ae9b5dd9ae1b4..e8638a0fcaf73e4500469f368ef9494e495099b3)
* [`ring_theory.multiplicity`@`ceb887ddf3344dab425292e497fa2af91498437c`..`e8638a0fcaf73e4500469f368ef9494e495099b3`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/multiplicity?range=ceb887ddf3344dab425292e497fa2af91498437c..e8638a0fcaf73e4500469f368ef9494e495099b3)



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
xroblot pushed a commit that referenced this pull request Apr 23, 2023
@YaelDillies @xroblot
feat(algebra/divisibility/basic): Dot notation aliases (#18698)
f097e58 
A few convenience shortcuts for `dvd` along with some simple `nat` lemmas. Also
* Drop `neg_dvd_of_dvd`/`dvd_of_neg_dvd`/`dvd_neg_of_dvd`/`dvd_of_dvd_neg` in favor of the aforementioned shortcuts.
* Remove explicit arguments to `dvd_neg`/`neg_dvd`.
* Drop `int.of_nat_dvd_of_dvd_nat_abs`/`int.dvd_nat_abs_of_of_nat_dvd` because they are the two directions of `int.coe_nat_dvd_left`.
* Move `group_with_zero.to_cancel_monoid_with_zero` from `algebra.group_with_zero.units.basic` back to `algebra.group_with_zero.basic`. It was erroneously moved during the Great Splits.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@YaelDillies @semorrison @eric-wieser @Vierkantor @leanprover-community-bot-assistant