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(data/multiset/basic): add some lemmas #8787

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(data/multiset/basic): add some lemmas #8787

wants to merge 11 commits into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde commented Aug 21, 2021 •
edited by jcommelin
Loading

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 21, 2021
Ruben-VandeVelde and others added 2 commits August 21, 2021 21:54
@Ruben-VandeVelde
feat(data/multiset/basic): add countp_cons
8e75071
@Ruben-VandeVelde @jcommelin
feat(data/multiset/basic): add countp_map
f074945 
Statement from #3169.

Co-authored-by: Johan Commelin <johan@commelin.net>
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Aug 21, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 22, 2021
@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-review The author would like community review of the PR label Aug 22, 2021
@jcommelin
Copy link
Member

LGTM

bors d+

@bors
Copy link

bors bot commented Aug 26, 2021

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

@github-actions github-actions bot 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 Aug 26, 2021
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Aug 26, 2021
bors bot pushed a commit that referenced this pull request Aug 26, 2021
@Ruben-VandeVelde @jcommelin
feat(data/multiset/basic): add some lemmas (#8787)
b7212dd 


Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Aug 26, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 26, 2021
@Ruben-VandeVelde @jcommelin
feat(data/multiset/basic): add some lemmas (#8787)
83490fc 


Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Aug 26, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/multiset/basic): add some lemmas [Merged by Bors] - feat(data/multiset/basic): add some lemmas Aug 26, 2021
@bors bors bot closed this Aug 26, 2021
@bors bors bot deleted the multiset-lemmas branch August 26, 2021 21:24
@YaelDillies YaelDillies mentioned this pull request Mar 28, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 5, 2024
@YaelDillies
chore: Sort big operator order lemmas (#11750)
3cc22ef 
Take the content of
* some of `Algebra.BigOperators.List.Basic`
* some of `Algebra.BigOperators.List.Lemmas`
* some of `Algebra.BigOperators.Multiset.Basic`
* some of `Algebra.BigOperators.Multiset.Lemmas`
* `Algebra.BigOperators.Multiset.Order`
* `Algebra.BigOperators.Order`

and sort it into six files:
* `Algebra.Order.BigOperators.Group.List`. I credit Yakov for leanprover-community/mathlib#8543.
* `Algebra.Order.BigOperators.Group.Multiset`. Copyright inherited from `Algebra.BigOperators.Multiset.Order`.
* `Algebra.Order.BigOperators.Group.Finset`. Copyright inherited from `Algebra.BigOperators.Order`.
* `Algebra.Order.BigOperators.Ring.List`. I credit Stuart for leanprover-community/mathlib#10184.
* `Algebra.Order.BigOperators.Ring.Multiset`. I credit Ruben for leanprover-community/mathlib#8787.
* `Algebra.Order.BigOperators.Ring.Finset`. I credit Floris for leanprover-community/mathlib#1294.

Here are the design decisions at play:
* Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import `Data.Nat.Order.Basic` in a few `List` files.
* It's `Algebra.Order.BigOperators` instead of `Algebra.BigOperators.Order` because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
* There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under `Algebra.Order.BigOperators.Group` should be additivisable (except a few `Nat`- or `Int`-specific lemmas). In contrast, things under `Algebra.Order.BigOperators.Ring` are more prone to having heavy imports.
* Lemmas are separated according to `List` vs `Multiset` vs `Finset`. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the `AbsoluteValue` lemmas from `Algebra.Order.BigOperators.Ring.Finset` to a file `Algebra.Order.BigOperators.Ring.AbsoluteValue` and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files `Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset`, `Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset`, etc...
* `Finsupp` big operator and `finprod`/`finsum` order lemmas also belong in `Algebra.Order.BigOperators`. I haven't done so in this PR because the diff is big enough like that.
Louddy pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 15, 2024
@YaelDillies @Louddy
chore: Sort big operator order lemmas (#11750)
e20948c 
Take the content of
* some of `Algebra.BigOperators.List.Basic`
* some of `Algebra.BigOperators.List.Lemmas`
* some of `Algebra.BigOperators.Multiset.Basic`
* some of `Algebra.BigOperators.Multiset.Lemmas`
* `Algebra.BigOperators.Multiset.Order`
* `Algebra.BigOperators.Order`

and sort it into six files:
* `Algebra.Order.BigOperators.Group.List`. I credit Yakov for leanprover-community/mathlib#8543.
* `Algebra.Order.BigOperators.Group.Multiset`. Copyright inherited from `Algebra.BigOperators.Multiset.Order`.
* `Algebra.Order.BigOperators.Group.Finset`. Copyright inherited from `Algebra.BigOperators.Order`.
* `Algebra.Order.BigOperators.Ring.List`. I credit Stuart for leanprover-community/mathlib#10184.
* `Algebra.Order.BigOperators.Ring.Multiset`. I credit Ruben for leanprover-community/mathlib#8787.
* `Algebra.Order.BigOperators.Ring.Finset`. I credit Floris for leanprover-community/mathlib#1294.

Here are the design decisions at play:
* Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import `Data.Nat.Order.Basic` in a few `List` files.
* It's `Algebra.Order.BigOperators` instead of `Algebra.BigOperators.Order` because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
* There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under `Algebra.Order.BigOperators.Group` should be additivisable (except a few `Nat`- or `Int`-specific lemmas). In contrast, things under `Algebra.Order.BigOperators.Ring` are more prone to having heavy imports.
* Lemmas are separated according to `List` vs `Multiset` vs `Finset`. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the `AbsoluteValue` lemmas from `Algebra.Order.BigOperators.Ring.Finset` to a file `Algebra.Order.BigOperators.Ring.AbsoluteValue` and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files `Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset`, `Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset`, etc...
* `Finsupp` big operator and `finprod`/`finsum` order lemmas also belong in `Algebra.Order.BigOperators`. I haven't done so in this PR because the diff is big enough like that.
atarnoam pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 16, 2024
@YaelDillies @atarnoam
chore: Sort big operator order lemmas (#11750)
d5eb87a 
Take the content of
* some of `Algebra.BigOperators.List.Basic`
* some of `Algebra.BigOperators.List.Lemmas`
* some of `Algebra.BigOperators.Multiset.Basic`
* some of `Algebra.BigOperators.Multiset.Lemmas`
* `Algebra.BigOperators.Multiset.Order`
* `Algebra.BigOperators.Order`

and sort it into six files:
* `Algebra.Order.BigOperators.Group.List`. I credit Yakov for leanprover-community/mathlib#8543.
* `Algebra.Order.BigOperators.Group.Multiset`. Copyright inherited from `Algebra.BigOperators.Multiset.Order`.
* `Algebra.Order.BigOperators.Group.Finset`. Copyright inherited from `Algebra.BigOperators.Order`.
* `Algebra.Order.BigOperators.Ring.List`. I credit Stuart for leanprover-community/mathlib#10184.
* `Algebra.Order.BigOperators.Ring.Multiset`. I credit Ruben for leanprover-community/mathlib#8787.
* `Algebra.Order.BigOperators.Ring.Finset`. I credit Floris for leanprover-community/mathlib#1294.

Here are the design decisions at play:
* Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import `Data.Nat.Order.Basic` in a few `List` files.
* It's `Algebra.Order.BigOperators` instead of `Algebra.BigOperators.Order` because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
* There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under `Algebra.Order.BigOperators.Group` should be additivisable (except a few `Nat`- or `Int`-specific lemmas). In contrast, things under `Algebra.Order.BigOperators.Ring` are more prone to having heavy imports.
* Lemmas are separated according to `List` vs `Multiset` vs `Finset`. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the `AbsoluteValue` lemmas from `Algebra.Order.BigOperators.Ring.Finset` to a file `Algebra.Order.BigOperators.Ring.AbsoluteValue` and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files `Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset`, `Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset`, etc...
* `Finsupp` big operator and `finprod`/`finsum` order lemmas also belong in `Algebra.Order.BigOperators`. I haven't done so in this PR because the diff is big enough like that.
uniwuni pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 19, 2024
@YaelDillies @uniwuni
chore: Sort big operator order lemmas (#11750)
1b43f98 
Take the content of
* some of `Algebra.BigOperators.List.Basic`
* some of `Algebra.BigOperators.List.Lemmas`
* some of `Algebra.BigOperators.Multiset.Basic`
* some of `Algebra.BigOperators.Multiset.Lemmas`
* `Algebra.BigOperators.Multiset.Order`
* `Algebra.BigOperators.Order`

and sort it into six files:
* `Algebra.Order.BigOperators.Group.List`. I credit Yakov for leanprover-community/mathlib#8543.
* `Algebra.Order.BigOperators.Group.Multiset`. Copyright inherited from `Algebra.BigOperators.Multiset.Order`.
* `Algebra.Order.BigOperators.Group.Finset`. Copyright inherited from `Algebra.BigOperators.Order`.
* `Algebra.Order.BigOperators.Ring.List`. I credit Stuart for leanprover-community/mathlib#10184.
* `Algebra.Order.BigOperators.Ring.Multiset`. I credit Ruben for leanprover-community/mathlib#8787.
* `Algebra.Order.BigOperators.Ring.Finset`. I credit Floris for leanprover-community/mathlib#1294.

Here are the design decisions at play:
* Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import `Data.Nat.Order.Basic` in a few `List` files.
* It's `Algebra.Order.BigOperators` instead of `Algebra.BigOperators.Order` because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
* There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under `Algebra.Order.BigOperators.Group` should be additivisable (except a few `Nat`- or `Int`-specific lemmas). In contrast, things under `Algebra.Order.BigOperators.Ring` are more prone to having heavy imports.
* Lemmas are separated according to `List` vs `Multiset` vs `Finset`. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the `AbsoluteValue` lemmas from `Algebra.Order.BigOperators.Ring.Finset` to a file `Algebra.Order.BigOperators.Ring.AbsoluteValue` and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files `Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset`, `Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset`, etc...
* `Finsupp` big operator and `finprod`/`finsum` order lemmas also belong in `Algebra.Order.BigOperators`. I haven't done so in this PR because the diff is big enough like that.
callesonne pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 22, 2024
@YaelDillies @callesonne
chore: Sort big operator order lemmas (#11750)
19bc29d 
Take the content of
* some of `Algebra.BigOperators.List.Basic`
* some of `Algebra.BigOperators.List.Lemmas`
* some of `Algebra.BigOperators.Multiset.Basic`
* some of `Algebra.BigOperators.Multiset.Lemmas`
* `Algebra.BigOperators.Multiset.Order`
* `Algebra.BigOperators.Order`

and sort it into six files:
* `Algebra.Order.BigOperators.Group.List`. I credit Yakov for leanprover-community/mathlib#8543.
* `Algebra.Order.BigOperators.Group.Multiset`. Copyright inherited from `Algebra.BigOperators.Multiset.Order`.
* `Algebra.Order.BigOperators.Group.Finset`. Copyright inherited from `Algebra.BigOperators.Order`.
* `Algebra.Order.BigOperators.Ring.List`. I credit Stuart for leanprover-community/mathlib#10184.
* `Algebra.Order.BigOperators.Ring.Multiset`. I credit Ruben for leanprover-community/mathlib#8787.
* `Algebra.Order.BigOperators.Ring.Finset`. I credit Floris for leanprover-community/mathlib#1294.

Here are the design decisions at play:
* Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import `Data.Nat.Order.Basic` in a few `List` files.
* It's `Algebra.Order.BigOperators` instead of `Algebra.BigOperators.Order` because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
* There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under `Algebra.Order.BigOperators.Group` should be additivisable (except a few `Nat`- or `Int`-specific lemmas). In contrast, things under `Algebra.Order.BigOperators.Ring` are more prone to having heavy imports.
* Lemmas are separated according to `List` vs `Multiset` vs `Finset`. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the `AbsoluteValue` lemmas from `Algebra.Order.BigOperators.Ring.Finset` to a file `Algebra.Order.BigOperators.Ring.AbsoluteValue` and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files `Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset`, `Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset`, etc...
* `Finsupp` big operator and `finprod`/`finsum` order lemmas also belong in `Algebra.Order.BigOperators`. I haven't done so in this PR because the diff is big enough like that.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@Ruben-VandeVelde @jcommelin