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: basic results about Finset.sym2 #14212

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat: basic results about Finset.sym2 #14212

wants to merge 36 commits into from

Commits on Jun 28, 2024

  1. feat: add results about Finset.cons and Finset.sym2

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    86e661e View commit details
    Browse the repository at this point in the history

  2. golf

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    729ef94 View commit details
    Browse the repository at this point in the history

  3. bundle map

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    d5524fb View commit details
    Browse the repository at this point in the history

  4. wanted

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    31b35d0 View commit details
    Browse the repository at this point in the history

  5. repr instance

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    91b63f6 View commit details
    Browse the repository at this point in the history

  6. more proof_wanted

    @eric-wieser
    eric-wieser committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    7316baf View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2024

  1. proof no longer wanted

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    cdb5ea2 View commit details
    Browse the repository at this point in the history

  2. extract to another PR

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    9bbadbf View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Data/List/Sym.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @eric-wieser @github-actions
    eric-wieser and github-actions[bot] authored Jun 29, 2024
    Configuration menu
    Copy the full SHA
    6cbae05 View commit details
    Browse the repository at this point in the history

  4. revert

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    77a0e0d View commit details
    Browse the repository at this point in the history

  5. Merge branch 'eric-wieser/sym2-lemmas' of https://github.com/leanprov… 

    …er-community/mathlib4 into eric-wieser/sym2-lemmas
    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    36901d3 View commit details
    Browse the repository at this point in the history

  6. more results

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    ab65f49 View commit details
    Browse the repository at this point in the history

  7. move

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    2b440bc View commit details
    Browse the repository at this point in the history

  8. import

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    e2735aa View commit details
    Browse the repository at this point in the history

  9. golf

    @eric-wieser
    eric-wieser committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    8831552 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2024

  1. feat(Data/List): dedup and union lemmas

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    9a9ca48 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'eric-wieser/dedup-lemmas' into eric-wieser/sym2-lemmas

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    b65d54e View commit details
    Browse the repository at this point in the history

  3. more lemmas

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    a1c93ed View commit details
    Browse the repository at this point in the history

  4. a few more

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    105f1d2 View commit details
    Browse the repository at this point in the history

  5. fix name

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    cd7fb1e View commit details
    Browse the repository at this point in the history

  6. and another

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    6fbd2fb View commit details
    Browse the repository at this point in the history

  7. and another

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    0f985e4 View commit details
    Browse the repository at this point in the history

  8. oops

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    d1bcfa9 View commit details
    Browse the repository at this point in the history

  9. whitespace

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    3a10a05 View commit details
    Browse the repository at this point in the history

  10. golf

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    e07e06d View commit details
    Browse the repository at this point in the history

  11. golf

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    880b343 View commit details
    Browse the repository at this point in the history

  12. style

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    271accf View commit details
    Browse the repository at this point in the history

  13. typo

    @eric-wieser
    eric-wieser committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    6372dff View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2024

  1. Add Yael's lemma

    @eric-wieser
    eric-wieser committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    e5a59c8 View commit details
    Browse the repository at this point in the history

  2. @golf@

    @eric-wieser
    eric-wieser committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    fdbd259 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. typeo

    @eric-wieser
    eric-wieser committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    d1662a5 View commit details
    Browse the repository at this point in the history

  2. golf

    @eric-wieser
    eric-wieser committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    179ad54 View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

  1. Merge remote-tracking branch 'origin/eric-wieser/dedup-lemmas' into e… 

    …ric-wieser/sym2-lemmas
    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    94611a0 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into eric-wieser/sym2-le… 

    …mmas
    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    48efe8c View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    be4d3a5 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2024

  1. golfs

    @eric-wieser
    eric-wieser committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    c2f79ef View commit details
    Browse the repository at this point in the history