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

Commits on Jul 22, 2023

  1. add power sums and most of proof of Newton's Identities from Zeilberger

    Michael Lee committed Jul 22, 2023
    Configuration menu
    Copy the full SHA
    4c649ce View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into michaellee94/newton

    Michael Lee committed Jul 22, 2023
    Configuration menu
    Copy the full SHA
    e6b0c8c View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2023

  1. fix some formatting, finish ridiculous subtraction lemma

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    b2926aa View commit details
    Browse the repository at this point in the history

  2. add stub of theorem for disjoint subsets

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    0fab8d7 View commit details
    Browse the repository at this point in the history

  3. proof of disjointness

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    4a5e043 View commit details
    Browse the repository at this point in the history

  4. add proof of union eq

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    b109afd View commit details
    Browse the repository at this point in the history

  5. prove disjoint union

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    84c911b View commit details
    Browse the repository at this point in the history

  6. delete fintype_card

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    bdb0258 View commit details
    Browse the repository at this point in the history

  7. finish the proof of esymm_to_weight

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    39804f1 View commit details
    Browse the repository at this point in the history

  8. add the proofs of sum equivs

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    c753557 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into michaellee94/newton

    Michael Lee committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    8220424 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. fill in some of proof of sum_equiv_lt_k

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4edf892 View commit details
    Browse the repository at this point in the history

  2. delete unnecessary theorem

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    eda5018 View commit details
    Browse the repository at this point in the history

  3. finish proof of sum_equiv_lt_k

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    2a094f6 View commit details
    Browse the repository at this point in the history

  4. finish esymm_mult_psum_summand_to_weight

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    a638a5f View commit details
    Browse the repository at this point in the history

  5. some minor simplifications

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    29a0b7c View commit details
    Browse the repository at this point in the history

  6. this actually covers both cases under the convention that esymm is ze… 

    …ro for param larger than n
    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    b8fa6a2 View commit details
    Browse the repository at this point in the history

  7. add proof of NewtonIdentity

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5e3541b View commit details
    Browse the repository at this point in the history

  8. move this theorem earlier

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    14bd6b6 View commit details
    Browse the repository at this point in the history

  9. finish proof

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7187c8b View commit details
    Browse the repository at this point in the history

  10. Merge branch 'master' into michaellee94/newton

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c85f16e View commit details
    Browse the repository at this point in the history

  11. add new module

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    f5a6f12 View commit details
    Browse the repository at this point in the history

  12. documentation

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4339d06 View commit details
    Browse the repository at this point in the history

  13. updated undergrad math list

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c8c8dce View commit details
    Browse the repository at this point in the history

  14. fix linter error

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d814dc0 View commit details
    Browse the repository at this point in the history

  15. add citation

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7b71521 View commit details
    Browse the repository at this point in the history

  16. add docstring here

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    68f2ad6 View commit details
    Browse the repository at this point in the history

  17. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @eric-wieser
    michaellee94 and eric-wieser committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e2fe0ee View commit details
    Browse the repository at this point in the history

  18. fix univ sum notation and universe polymorphism

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    f16ab13 View commit details
    Browse the repository at this point in the history

  19. pascal case for PairsPred

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    b9a9def View commit details
    Browse the repository at this point in the history

  20. let's make this a namespace, and only open Classical in theorems dire… 

    …ctly using PairsPred
    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    ffbe0a0 View commit details
    Browse the repository at this point in the history

  21. fix docstring

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    700b807 View commit details
    Browse the repository at this point in the history

  22. change name here too

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c33018a View commit details
    Browse the repository at this point in the history

  23. fix indentation here

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    87d1c47 View commit details
    Browse the repository at this point in the history

  24. mult -> mul

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5478b7d View commit details
    Browse the repository at this point in the history

  25. remove unused theorem

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    dc8434d View commit details
    Browse the repository at this point in the history

  26. add contrapositive here

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    0f7cdd6 View commit details
    Browse the repository at this point in the history

  27. remove by exact

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    fc8e3b5 View commit details
    Browse the repository at this point in the history

  28. close namespace

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    bc4063a View commit details
    Browse the repository at this point in the history

  29. put classical tactic inside theorems

    Michael Lee committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    28cbea3 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2023

  1. prove that MvPolynomial is a CharZero if R is a CharZero

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    8a715e6 View commit details
    Browse the repository at this point in the history

  2. begin removing generic simps

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    6d093f2 View commit details
    Browse the repository at this point in the history

  3. use one-liner here from ericrbg

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    5b54731 View commit details
    Browse the repository at this point in the history

  4. additional rewrites to eliminate simp, simp_rw, and simp_all that don… 

    …'t close goals (excepting simp only)
    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    1e9bc84 View commit details
    Browse the repository at this point in the history

  5. insert -> cons

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    4913fc4 View commit details
    Browse the repository at this point in the history

  6. remove unused variable here

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    7042f78 View commit details
    Browse the repository at this point in the history

  7. delete PairsPred and inline predicate

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    83d4360 View commit details
    Browse the repository at this point in the history

  8. Merge pull request #6138 from michaellee94/michaellee94/newton 

    merge from michaellee94/newton
    michaellee94 committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    a0e063f View commit details
    Browse the repository at this point in the history

  9. don't need this variable specification here, I think

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    2669410 View commit details
    Browse the repository at this point in the history

  10. fix stuff with namespaces

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    2578e54 View commit details
    Browse the repository at this point in the history

  11. correct namespace here

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    374887a View commit details
    Browse the repository at this point in the history

  12. we actually don't need T_map_restr

    Michael Lee committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    b4c5d0a View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. address linter error

    Michael Lee committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    e7b9165 View commit details
    Browse the repository at this point in the history

  2. move the section and namespace declarations around to make MvPolynomi… 

    …al.psum work, and explain what psum is exactly
    Michael Lee committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    619357a View commit details
    Browse the repository at this point in the history

  3. tweak some names and parens, and golf

    @eric-wieser
    eric-wieser committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    6c9956d View commit details
    Browse the repository at this point in the history

  4. address naming convention in T_map

    Michael Lee committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    fdf1cd5 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2023

  1. some golfing

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    6220fce View commit details
    Browse the repository at this point in the history

  2. a little more golfing

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    a3d9ea1 View commit details
    Browse the repository at this point in the history

  3. more golfing

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    246607f View commit details
    Browse the repository at this point in the history

  4. this nomenclature sort of makes more sense the other way around

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    657d78e View commit details
    Browse the repository at this point in the history

  5. simplify proof here

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    967cdac View commit details
    Browse the repository at this point in the history

  6. more golf

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    40832fc View commit details
    Browse the repository at this point in the history

  7. explicit left/right notation for ands

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    53cacb6 View commit details
    Browse the repository at this point in the history

  8. more golf

    Michael Lee committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    6c3f91c View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2023

  1. consistent notation

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    3ccbe44 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into michaellee94/newton-identities

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    10a635a View commit details
    Browse the repository at this point in the history

  3. drop unnecessary notation part

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    4befce4 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
    @michaellee94 @ericrbg
    michaellee94 and ericrbg committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    6ebc5a2 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
    @michaellee94 @ericrbg
    michaellee94 and ericrbg committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    5a2e658 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
    @michaellee94 @ericrbg
    michaellee94 and ericrbg committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    d5fb359 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
    @michaellee94 @ericrbg
    michaellee94 and ericrbg committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    57fd9be View commit details
    Browse the repository at this point in the history

  8. remove unnecessary comment here

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    f9a2f1c View commit details
    Browse the repository at this point in the history

  9. use nice dot notation here

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    cfbc7b6 View commit details
    Browse the repository at this point in the history

  10. address theorem vs def naming conventions, and make internal results … 

    …private
    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    1274467 View commit details
    Browse the repository at this point in the history

  11. add psum_recurrence

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    a43254e View commit details
    Browse the repository at this point in the history

  12. add psum_zero lemma

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    1c5ef46 View commit details
    Browse the repository at this point in the history

  13. standardize notation here

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    8ad1daf View commit details
    Browse the repository at this point in the history

  14. add psum_one

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    15140d2 View commit details
    Browse the repository at this point in the history

  15. move these up

    Michael Lee committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    042248d View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2023

  1. fix notation here

    Michael Lee committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    5a1528e View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2023

  1. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    c4fdd48 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    d861aac View commit details
    Browse the repository at this point in the history

  3. more idiomatic names

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    cea7fa5 View commit details
    Browse the repository at this point in the history

  4. move the psum defs to Symmetric.lean

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    e44a7b9 View commit details
    Browse the repository at this point in the history

  5. change name here

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    07ed2a0 View commit details
    Browse the repository at this point in the history

  6. slightly shorter proof here

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    01eed7a View commit details
    Browse the repository at this point in the history

  7. rewrite split_ifs to instead be rcases and use the lemmas about pairMap

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    0e38722 View commit details
    Browse the repository at this point in the history

  8. standardize notation here

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    b3090e5 View commit details
    Browse the repository at this point in the history

  9. use psum_def here

    Michael Lee committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    f909c7a View commit details
    Browse the repository at this point in the history

  10. Some golfing

    @ocfnash
    ocfnash committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    b1c6bf2 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2023

  1. use antidiagonal instead of subtraction on the natural numbers

    Michael Lee committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    63574de View commit details
    Browse the repository at this point in the history

  2. Update undergrad.yaml 

    Fix name of declaration here
    @michaellee94
    michaellee94 committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    54ac90b View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    03c7461 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    9e911f6 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    237c814 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    ec7616e View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    ec940a1 View commit details
    Browse the repository at this point in the history

  8. fix spacing here

    Michael Lee committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    2153551 View commit details
    Browse the repository at this point in the history

  9. Set.Ioo rather than two filters here

    Michael Lee committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    b1d6aa3 View commit details
    Browse the repository at this point in the history

  10. tweak namespace

    Michael Lee committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    e1247c2 View commit details
    Browse the repository at this point in the history

  11. brief explanation of proof

    Michael Lee committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    aa7ef2e View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2023

  1. Merge branch 'master' into michaellee94/newton-identities

    @ocfnash
    ocfnash committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    0453a12 View commit details
    Browse the repository at this point in the history

  2. Fix after merging master 

    Necessary because of:
#6528
#6499
    @ocfnash
    ocfnash committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    27d8c0e View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2023

  1. remove CharZero and NoZeroDivisors assumptions

    Michael Lee committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    c2b2245 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean 

    Co-authored-by: Oliver Nash <github@olivernash.org>
    @michaellee94 @ocfnash
    michaellee94 and ocfnash committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    e5e91e8 View commit details
    Browse the repository at this point in the history

  3. expand docstring slightly

    Michael Lee committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    6dd66ad View commit details
    Browse the repository at this point in the history