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 Algebra.BigOperators.Fin #1848

Closed
wants to merge 35 commits into from
Closed

[Merged by Bors] - feat: port Algebra.BigOperators.Fin #1848

wants to merge 35 commits into from

Commits on Jan 26, 2023

  1. feat: port Data.Fin.Interval

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    533ab2c View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    fc59bfc View commit details
    Browse the repository at this point in the history

  3. script output

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    1723092 View commit details
    Browse the repository at this point in the history

  4. update Mathlib.lean

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    5813dc0 View commit details
    Browse the repository at this point in the history

  5. fixes

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    6f0b760 View commit details
    Browse the repository at this point in the history

  6. feat: port Data.Fintype.Fin

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    0d69f36 View commit details
    Browse the repository at this point in the history

  7. Initial file copy from mathport

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    9f2e994 View commit details
    Browse the repository at this point in the history

  8. script output

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7e9c619 View commit details
    Browse the repository at this point in the history

  9. update Mathlib.lean

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    95987e9 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'port/Data.Fin.Interval' into port/Data.Fintype.Fin

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

  11. fixes

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    f9bdd67 View commit details
    Browse the repository at this point in the history

  12. feat: port Algebra.BigOperators.Fin

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7af614b View commit details
    Browse the repository at this point in the history

  13. Initial file copy from mathport

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7c38fc4 View commit details
    Browse the repository at this point in the history

  14. script output

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7fbfc9c View commit details
    Browse the repository at this point in the history

  15. update Mathlib.lean

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    317d67a View commit details
    Browse the repository at this point in the history

  16. Merge branch 'port/Data.Fintype.Fin' into port/Algebra.BigOperators.Fin

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    cc318cd View commit details
    Browse the repository at this point in the history

  17. partial fixes

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    8789f4c View commit details
    Browse the repository at this point in the history

  18. re-add limited tracing with to_additive_detail, fix bug

    @fpvandoorn
    fpvandoorn committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    ef7b665 View commit details
    Browse the repository at this point in the history

  19. partial fixes

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7b808ef View commit details
    Browse the repository at this point in the history

  20. Merge branch 'master' into port/Algebra.BigOperators.Fin

    @joneugster
    joneugster committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    a0018b5 View commit details
    Browse the repository at this point in the history

  21. another fix

    @fpvandoorn
    fpvandoorn committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    649332a View commit details
    Browse the repository at this point in the history

  22. update doc, finish debug trace

    @fpvandoorn
    fpvandoorn committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    53c9474 View commit details
    Browse the repository at this point in the history

  23. -newlines

    @fpvandoorn
    fpvandoorn committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    b4d917a View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2023

  1. struggling

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    318ecd2 View commit details
    Browse the repository at this point in the history

  2. docfix

    @fpvandoorn
    fpvandoorn committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    58af617 View commit details
    Browse the repository at this point in the history

  3. partial fix

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    4fd5775 View commit details
    Browse the repository at this point in the history

  4. fixes

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    52fcaa8 View commit details
    Browse the repository at this point in the history

  5. merge toadditive bug fix

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    8d58200 View commit details
    Browse the repository at this point in the history

  6. lint

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    55ef1e6 View commit details
    Browse the repository at this point in the history

  7. fix lints script

    @joneugster
    joneugster committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    2c3bbe0 View commit details
    Browse the repository at this point in the history

  8. lint

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

  9. lint

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

Commits on Feb 1, 2023

  1. Update Mathlib/Algebra/BigOperators/Fin.lean

    @jcommelin
    jcommelin committed Feb 1, 2023
    Configuration menu
    Copy the full SHA
    27022ce View commit details
    Browse the repository at this point in the history

  2. locale BigOperators works again

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

  3. Merge branch 'master' into port/Algebra.BigOperators.Fin

    @jcommelin
    jcommelin committed Feb 1, 2023
    Configuration menu
    Copy the full SHA
    8eaca11 View commit details
    Browse the repository at this point in the history