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: More big operator lemmas #10551

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat: More big operator lemmas #10551

wants to merge 26 commits into from

Conversation

YaelDillies
Copy link
Collaborator

From LeanAPAP

Open in Gitpod

github-actions[bot]
github-actions bot reviewed Feb 14, 2024
View reviewed changes
Mathlib/Algebra/BigOperators/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Pi.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Pi.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Feb 14, 2024
YaelDillies and others added 3 commits February 14, 2024 19:28
@YaelDillies @github-actions
Update Mathlib/Algebra/BigOperators/Basic.lean
2ac4370 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@YaelDillies @github-actions
Update Mathlib/Algebra/BigOperators/Pi.lean
af812f7 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@YaelDillies @github-actions
Update Mathlib/Algebra/BigOperators/Pi.lean
479cec9 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
github-actions[bot]
github-actions bot reviewed Feb 14, 2024
View reviewed changes
Mathlib/Algebra/BigOperators/Pi.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Pi.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies mentioned this pull request Feb 14, 2024
Open
1 task
eric-wieser
eric-wieser reviewed Feb 25, 2024
View reviewed changes
Mathlib/Algebra/BigOperators/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Basic.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies mentioned this pull request Mar 21, 2024
Open
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 15, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 15, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Apr 29, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Looks okay for as far as I understand what's going on :)

Mathlib/Algebra/BigOperators/Basic.lean
@@ -2256,6 +2293,52 @@ theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid
#align fintype.prod_subtype_mul_prod_subtype Fintype.prod_subtype_mul_prod_subtype
#align fintype.sum_subtype_add_sum_subtype Fintype.sum_subtype_add_sum_subtype

@[to_additive] lemma prod_subset {s : Finset ι} {f : ι → α} (h : ∀ i, f i ≠ 1 → i ∈ s) :
Copy link
Collaborator

Choose a reason for hiding this comment

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

Any reason not to match x ∉ s₁ → f x = 1 from Finset.prod_subset?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It's much more useful this way, I find, as it can be interpreted as saying that the support of f is a subset of s. Finset.prod_subset can't really afford to be stated like that as it instead wants to emphasize s₁ \ s₂.

Mathlib/Data/Finset/Union.lean Outdated Show resolved Hide resolved
kbuzzard
kbuzzard approved these changes Apr 29, 2024
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

I don't really know this part of the library but the code/naming etc looks fine.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 29, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 29, 2024
@Ruben-VandeVelde
Copy link
Collaborator

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

jcommelin
jcommelin approved these changes Apr 30, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@YaelDillies
feat: More big operator lemmas (#10551)
db6bc5d 
From LeanAPAP
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: More big operator lemmas [Merged by Bors] - feat: More big operator lemmas Apr 30, 2024
@mathlib-bors mathlib-bors bot closed this Apr 30, 2024
@mathlib-bors mathlib-bors bot deleted the prod_fiberwise_eq_prod_filter branch April 30, 2024 06:07
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@YaelDillies @apnelson1
feat: More big operator lemmas (#10551)
62dd6a3 
From LeanAPAP
callesonne pushed a commit that referenced this pull request May 16, 2024
@YaelDillies @callesonne
feat: More big operator lemmas (#10551)
727d7e2 
From LeanAPAP
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@github-actions github-actions[bot] github-actions left review comments

@jcommelin jcommelin jcommelin approved these changes

@kbuzzard kbuzzard kbuzzard approved these changes

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. 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
6 participants
@YaelDillies @Ruben-VandeVelde @eric-wieser @jcommelin @kbuzzard @leanprover-community-mathlib4-bot