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 Combinatorics.HalesJewett #1704

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat: port Combinatorics.HalesJewett #1704

wants to merge 22 commits into from

Commits on Jan 20, 2023

  1. feat: port Combinatorics.HalesJewett

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    7d2b022 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    386d24e 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
    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    a3e3aa2 View commit details
    Browse the repository at this point in the history

  4. starting

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    ffb1957 View commit details
    Browse the repository at this point in the history

  5. first pass

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    c7f7d02 View commit details
    Browse the repository at this point in the history

  6. Inhabited

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    3c1a61e View commit details
    Browse the repository at this point in the history

  7. some => choose

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    450219b View commit details
    Browse the repository at this point in the history

  8. map_apply add rfl

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    ccb45e0 View commit details
    Browse the repository at this point in the history

  9. fix empty case

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    61c4ff7 View commit details
    Browse the repository at this point in the history

  10. manual linebreaks

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    868aff2 View commit details
    Browse the repository at this point in the history

  11. one more line break

    @mo271
    mo271 committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    8e1190c View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2023

  1. Merge branch 'master' into port/Combinatorics.HalesJewett

    @mo271
    mo271 committed Jan 21, 2023
    Configuration menu
    Copy the full SHA
    88e424f View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2023

  1. Merge branch 'master' into port/Combinatorics.HalesJewett

    @mo271
    mo271 committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    b1e50d6 View commit details
    Browse the repository at this point in the history

  2. some parts towards the end

    @mo271
    mo271 committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    5d7dece View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2023

  1. continue

    @mo271
    mo271 committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    82f0a50 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2023

  1. Merge remote-tracking branch 'origin' into port/Combinatorics.HalesJe… 

    …wett
    @LukasMias
    LukasMias committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    e251500 View commit details
    Browse the repository at this point in the history

  2. fixes

    @LukasMias
    LukasMias committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    b47be31 View commit details
    Browse the repository at this point in the history

  3. added docstrings

    @LukasMias
    LukasMias committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    934efd9 View commit details
    Browse the repository at this point in the history

  4. fixed old docstrings

    @LukasMias
    LukasMias committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    863a0c3 View commit details
    Browse the repository at this point in the history

  5. long line

    @LukasMias
    LukasMias committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    0ae7d55 View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2023

  1. docstring for idxfun

    @dwarn
    dwarn committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    15b092a View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2023

  1. Update Mathlib/Combinatorics/HalesJewett.lean

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    8635d59 View commit details
    Browse the repository at this point in the history