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 AlgebraicTopology.DoldKan.NCompGamma #3576

Closed
wants to merge 39 commits into from
Closed

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.NCompGamma #3576

wants to merge 39 commits into from

Commits on Apr 21, 2023

  1. feat: port AlgebraicTopology.DoldKan.Degeneracies

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    bd6858c View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    227a8d2 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
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    cdcd07a View commit details
    Browse the repository at this point in the history

  4. started working on this file

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    6053e8e View commit details
    Browse the repository at this point in the history

  5. it compiles

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    495f1fb View commit details
    Browse the repository at this point in the history

  6. feat: port AlgebraicTopology.DoldKan.SplitSimplicialObject

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    545b8f9 View commit details
    Browse the repository at this point in the history

  7. Initial file copy from mathport

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    75dbf1a View commit details
    Browse the repository at this point in the history

  8. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    6add734 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.D… 

    …egeneracies' into port/AlgebraicTopology.DoldKan.SplitSimplicialObject
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    617a068 View commit details
    Browse the repository at this point in the history

  10. it compiles

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    0f02de2 View commit details
    Browse the repository at this point in the history

  11. feat: port AlgebraicTopology.DoldKan.FunctorGamma

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    661663e View commit details
    Browse the repository at this point in the history

  12. Initial file copy from mathport

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    b9bfb64 View commit details
    Browse the repository at this point in the history

  13. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    e7b8ddd View commit details
    Browse the repository at this point in the history

  14. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.S… 

    …plitSimplicialObject' into port/AlgebraicTopology.DoldKan.FunctorGamma
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    5825b25 View commit details
    Browse the repository at this point in the history

  15. it compiles

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    fd57286 View commit details
    Browse the repository at this point in the history

  16. feat: port AlgebraicTopology.DoldKan.GammaCompN

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    25fb74d View commit details
    Browse the repository at this point in the history

  17. Initial file copy from mathport

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    a5d19ed View commit details
    Browse the repository at this point in the history

  18. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    c944ecd View commit details
    Browse the repository at this point in the history

  19. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.F… 

    …unctorGamma' into port/AlgebraicTopology.DoldKan.GammaCompN
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    678e9c7 View commit details
    Browse the repository at this point in the history

  20. started working on this file

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    a4a9d37 View commit details
    Browse the repository at this point in the history

  21. fixed a proof

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    78b5992 View commit details
    Browse the repository at this point in the history

  22. it compiles

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    7f76a84 View commit details
    Browse the repository at this point in the history

  23. feat: port AlgebraicTopology.DoldKan.NCompGamma

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    5751ad5 View commit details
    Browse the repository at this point in the history

  24. Initial file copy from mathport

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    770a42d View commit details
    Browse the repository at this point in the history

  25. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    aad624e View commit details
    Browse the repository at this point in the history

  26. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.G… 

    …ammaCompN' into port/AlgebraicTopology.DoldKan.NCompGamma
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    dbf0cf7 View commit details
    Browse the repository at this point in the history

  27. mostly done with this file

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    29b44a2 View commit details
    Browse the repository at this point in the history

  28. Merge remote-tracking branch 'origin' into port/AlgebraicTopology.Dol… 

    …dKan.GammaCompN
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    9e4dcf4 View commit details
    Browse the repository at this point in the history

  29. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.G… 

    …ammaCompN' into port/AlgebraicTopology.DoldKan.NCompGamma
    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    8dd2d0c View commit details
    Browse the repository at this point in the history

  30. it compiles but requires some cleanup

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    f7285e6 View commit details
    Browse the repository at this point in the history

  31. preventing a timeout

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    a324fad View commit details
    Browse the repository at this point in the history

  32. tidied a proof

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    e2ea996 View commit details
    Browse the repository at this point in the history

  33. better simps attributes

    @joelriou
    joelriou committed Apr 21, 2023
    Configuration menu
    Copy the full SHA
    ebfcaaa View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2023

  1. attribute [irreducible]

    @semorrison
    semorrison committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    e98e744 View commit details
    Browse the repository at this point in the history

  2. shortened a proof

    @joelriou
    joelriou committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    687984e View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.G… 

    …ammaCompN' into port/AlgebraicTopology.DoldKan.NCompGamma
    @joelriou
    joelriou committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    7dbe38d View commit details
    Browse the repository at this point in the history

  4. a few irreducible attributes

    @joelriou
    joelriou committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    ba0d93b View commit details
    Browse the repository at this point in the history

  5. trying to fix an error

    @joelriou
    joelriou committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    84e945f View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/master' into port/AlgebraicTopol… 

    …ogy.DoldKan.NCompGamma
    @semorrison
    semorrison committed Apr 22, 2023
    Configuration menu
    Copy the full SHA
    2d0f883 View commit details
    Browse the repository at this point in the history