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 CategoryTheory.Limits.Shapes.Diagonal #2881

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Diagonal #2881

wants to merge 15 commits into from

Commits on Mar 14, 2023

  1. feat: port CategoryTheory.Limits.Shapes.KernelPair

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    1fa830f View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    e1dd851 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 Mar 14, 2023
    Configuration menu
    Copy the full SHA
    c158e24 View commit details
    Browse the repository at this point in the history

  4. it compiles

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    10e1265 View commit details
    Browse the repository at this point in the history

  5. added PushoutCocone.IsColimit.desc

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    6bc339c View commit details
    Browse the repository at this point in the history

  6. feat: port CategoryTheory.Limits.Shapes.Diagonal

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    787dd56 View commit details
    Browse the repository at this point in the history

  7. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    b41aca4 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 Mar 14, 2023
    Configuration menu
    Copy the full SHA
    d827c86 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/port/CategoryTheory.Limits.Shape… 

    …s.KernelPair' into port/CategoryTheory.Limits.Shapes.Diagonal
    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    c7388c2 View commit details
    Browse the repository at this point in the history

  10. started working on this file

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    ac7f3fc View commit details
    Browse the repository at this point in the history

  11. it should compile

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    0acb2e6 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2023

  1. added set_option maxHeartbeats 400000

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    f2cb46d View commit details
    Browse the repository at this point in the history

  2. added set_option maxHeartbeats 400000 in

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    82a9980 View commit details
    Browse the repository at this point in the history

Commits on Mar 22, 2023

  1. Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits… 

    ….Shapes.Diagonal
    @joelriou
    joelriou committed Mar 22, 2023
    Configuration menu
    Copy the full SHA
    7aff1a9 View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2023

  1. using priorities on ext lemmas

    @joelriou
    joelriou committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    77f5bb2 View commit details
    Browse the repository at this point in the history