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(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's identities #6139

Closed
wants to merge 106 commits into from
Closed

[Merged by Bors] - feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's identities #6139

wants to merge 106 commits into from

Conversation

michaellee94
Copy link
Collaborator

Open in Gitpod

Michael Lee and others added 30 commits July 22, 2023 19:50
add power sums and most of proof of Newton's Identities from Zeilberger
4c649ce
Merge branch 'master' into michaellee94/newton
e6b0c8c
fix some formatting, finish ridiculous subtraction lemma
b2926aa
add stub of theorem for disjoint subsets
0fab8d7
proof of disjointness
4a5e043
add proof of union eq
b109afd
prove disjoint union
84c911b
delete fintype_card
bdb0258
finish the proof of esymm_to_weight
39804f1
add the proofs of sum equivs
c753557
Merge branch 'master' into michaellee94/newton
8220424
fill in some of proof of sum_equiv_lt_k
4edf892
delete unnecessary theorem
eda5018
finish proof of sum_equiv_lt_k
2a094f6
finish esymm_mult_psum_summand_to_weight
a638a5f
some minor simplifications
29a0b7c
this actually covers both cases under the convention that esymm is ze…
b8fa6a2 
…ro for param larger than n
add proof of NewtonIdentity
5e3541b
move this theorem earlier
14bd6b6
finish proof
7187c8b
Merge branch 'master' into michaellee94/newton
c85f16e
add new module
f5a6f12
documentation
4339d06
updated undergrad math list
c8c8dce
fix linter error
d814dc0
add citation
7b71521
add docstring here
68f2ad6
@eric-wieser
Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean
e2fe0ee 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
fix univ sum notation and universe polymorphism
f16ab13
pascal case for PairsPred
b9a9def
@michaellee94 michaellee94 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 Aug 11, 2023
This was referenced Aug 12, 2023
Closed
Closed
ocfnash
ocfnash approved these changes Aug 14, 2023
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

A few final suggestions. I think there's still quite a bit of scope for golfing the proofs but the statements of the main theorems are now great I think.

Thanks for all the work.

bors d+

Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean Show resolved Hide resolved
Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean Show resolved Hide resolved
Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Aug 14, 2023

✌️ michaellee94 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-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 15, 2023
@michaellee94 @ocfnash
feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's…
63ae2f4 
… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
@michaellee94
Copy link
Collaborator Author

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

bors r+

@bors
Copy link

bors bot commented Aug 15, 2023

Already running a review

@bors
Copy link

bors bot commented Aug 15, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's identities [Merged by Bors] - feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's identities Aug 15, 2023
@bors bors bot closed this Aug 15, 2023
@bors bors bot deleted the michaellee94/newton-identities branch August 15, 2023 05:56
semorrison pushed a commit that referenced this pull request Aug 15, 2023
@michaellee94 @ocfnash @semorrison
feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's…
7165b32 
… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
semorrison pushed a commit that referenced this pull request Aug 15, 2023
@michaellee94 @ocfnash @semorrison
feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's…
971bdf6 
… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
semorrison pushed a commit that referenced this pull request Aug 15, 2023
@michaellee94 @ocfnash @semorrison
feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's…
22bfdbe 
… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
semorrison pushed a commit that referenced this pull request Aug 17, 2023
@michaellee94 @ocfnash @semorrison
feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's…
692c4a1 
… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ocfnash ocfnash ocfnash approved these changes

@ericrbg ericrbg ericrbg approved these changes

@Ruben-VandeVelde Ruben-VandeVelde Awaiting requested review from Ruben-VandeVelde

@riccardobrasca riccardobrasca Awaiting requested review from riccardobrasca

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

Assignees
No one assigned
Labels
delegated new-feature Add features not present in Mathlib 3 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
@michaellee94 @riccardobrasca @eric-wieser @ocfnash @ericrbg @leanprover-community-mathlib4-bot