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(CategoryTheory): morphism properties that have the two-out-of-three property #12460

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat(CategoryTheory): morphism properties that have the two-out-of-three property #12460

wants to merge 21 commits into from

Commits on Apr 24, 2024

  1. split MorphismProperty.lean

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    33a8d3d View commit details
    Browse the repository at this point in the history

  2. fixing files

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    941de72 View commit details
    Browse the repository at this point in the history

  3. fixing the build

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    34e100c View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin' into morphism-property-split

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    2d3ba83 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin' into morphism-property-split

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    a5a4c79 View commit details
    Browse the repository at this point in the history

  6. the two out of three property

    @joelriou
    joelriou committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    16695f4 View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2024

  1. Merge remote-tracking branch 'origin' into morphism-property-split

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    3f174a3 View commit details
    Browse the repository at this point in the history

  2. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    f3ad8a1 View commit details
    Browse the repository at this point in the history

  3. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    37ae070 View commit details
    Browse the repository at this point in the history

  4. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    d3e7ce2 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/morphism-property-split' into tw… 

    …o-out-of-three-property
    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    960d095 View commit details
    Browse the repository at this point in the history

  6. fixed long line

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    105eea8 View commit details
    Browse the repository at this point in the history

  7. fixed docstring

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    a24362a View commit details
    Browse the repository at this point in the history

  8. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    b09608f View commit details
    Browse the repository at this point in the history

  9. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    d4d25a9 View commit details
    Browse the repository at this point in the history

  10. fixing the build

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    a13b6b2 View commit details
    Browse the repository at this point in the history

  11. fixing long line

    @joelriou
    joelriou committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    8d92967 View commit details
    Browse the repository at this point in the history

Commits on Apr 27, 2024

  1. Merge remote-tracking branch 'origin' into two-out-of-three-property

    @joelriou
    joelriou committed Apr 27, 2024
    Configuration menu
    Copy the full SHA
    e1d8066 View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2024

  1. Update Mathlib/CategoryTheory/MorphismProperty/Basic.lean 

    Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
    @joelriou @erdOne
    joelriou and erdOne authored Apr 28, 2024
    Configuration menu
    Copy the full SHA
    f7e9f54 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into two-out-of-three-property

    @joelriou
    joelriou committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    1491bf2 View commit details
    Browse the repository at this point in the history

  3. made IsStableUnderComposition.unop an instance

    @joelriou
    joelriou committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    70e66e2 View commit details
    Browse the repository at this point in the history