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: port SetTheory.Game.Basic #4311

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: port SetTheory.Game.Basic #4311

wants to merge 19 commits into from

Commits on Jun 25, 2023

  1. feat: port SetTheory.Game.Basic

    @QuinnLesquimau @digama0
    QuinnLesquimau authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    9c119be View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @QuinnLesquimau @digama0
    QuinnLesquimau authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    d0587c3 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @QuinnLesquimau @digama0
    QuinnLesquimau authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    7f0ad5d View commit details
    Browse the repository at this point in the history

  4. move setoid instance to PGame

    @QuinnLesquimau @digama0
    QuinnLesquimau authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    269e975 View commit details
    Browse the repository at this point in the history

  5. Correction of all the easy problems

    @QuinnLesquimau @digama0
    QuinnLesquimau authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    e255839 View commit details
    Browse the repository at this point in the history

  6. hmm, many errors remain

    @digama0
    Scott Morrison authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    eb7ca6b View commit details
    Browse the repository at this point in the history

  7. fix some problems

    @semorrison @digama0
    semorrison authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    a21edd2 View commit details
    Browse the repository at this point in the history

  8. fixes

    @semorrison @digama0
    semorrison authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    d93bc9f View commit details
    Browse the repository at this point in the history

  9. fix another

    @semorrison @digama0
    semorrison authored and digama0 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    19524b5 View commit details
    Browse the repository at this point in the history

  10. explicitly write out arguments to recursive calls in quot_left_distri… 

    …b and quot_mul_assoc
    @dwrensha
    dwrensha committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    c008589 View commit details
    Browse the repository at this point in the history

  11. placate the style linter

    @dwrensha
    dwrensha committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    2ca963c View commit details
    Browse the repository at this point in the history

  12. don't need the simp[invImage, InvImage]

    @dwrensha
    dwrensha committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    6517e09 View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2023

  1. Merge branch 'master' into port/SetTheory.Game.Basic

    @Parcly-Taxel
    Parcly-Taxel committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    89135b1 View commit details
    Browse the repository at this point in the history

  2. lint

    @Parcly-Taxel
    Parcly-Taxel committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    850893e View commit details
    Browse the repository at this point in the history

  3. cleanup

    @semorrison
    semorrison committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    c7a1333 View commit details
    Browse the repository at this point in the history

  4. Remove redundant lemmas

    @Parcly-Taxel
    Parcly-Taxel committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    3b2c4f1 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'port/SetTheory.Game.Basic' of github.com:leanprover-com… 

    …munity/mathlib4 into port/SetTheory.Game.Basic
    @Parcly-Taxel
    Parcly-Taxel committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    df6fe3c View commit details
    Browse the repository at this point in the history

  6. add link to lean4 issue

    @semorrison
    semorrison committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    30e7cfa View commit details
    Browse the repository at this point in the history

  7. Update Basic.lean

    @Parcly-Taxel
    Parcly-Taxel committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    5d7b872 View commit details
    Browse the repository at this point in the history