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 Mathlib.Data.List.Sigma #1493

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port Mathlib.Data.List.Sigma #1493

wants to merge 12 commits into from

Commits on Jan 11, 2023

  1. feat: port Mathlib.Data.List.Sigma

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

  2. Initial file copy from mathport

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

  3. Mathbin -> Mathlib; add import to Mathlib.lean

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

  4. starting

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

  5. first part of first pass

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

Commits on Jan 12, 2023

  1. some fixing

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    eb1d73c View commit details
    Browse the repository at this point in the history

  2. more fixing

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    5370684 View commit details
    Browse the repository at this point in the history

  3. more fixes

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    39d74b8 View commit details
    Browse the repository at this point in the history

  4. fixes

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    502b999 View commit details
    Browse the repository at this point in the history

  5. almost finished

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    a02a889 View commit details
    Browse the repository at this point in the history

  6. finished

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    ee7e130 View commit details
    Browse the repository at this point in the history

  7. line length

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    a09d8e7 View commit details
    Browse the repository at this point in the history