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: the pretriangulated structure on the opposite category #7336

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: the pretriangulated structure on the opposite category #7336

wants to merge 13 commits into from

Commits on Sep 23, 2023

  1. feat: the pretriangulated structure on the opposite category

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

  2. improving automation

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

  3. improving some proofs

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

  4. cleaning up

    @joelriou
    joelriou committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    8e94d30 View commit details
    Browse the repository at this point in the history

  5. dot notation

    @joelriou
    joelriou committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    69a281b View commit details
    Browse the repository at this point in the history

  6. fixing the build

    @joelriou
    joelriou committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    0be89a1 View commit details
    Browse the repository at this point in the history

  7. added docstring

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

Commits on Sep 25, 2023

  1. Merge remote-tracking branch 'origin' into pretriangulated-op

    @joelriou
    joelriou committed Sep 25, 2023
    Configuration menu
    Copy the full SHA
    7e21e51 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2023

  1. chore(CategoryTheory.Triangulated): use more camelCase for distTriang

    @joelriou
    joelriou committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    e99a67d View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2023

  1. Merge remote-tracking branch 'origin' into pretriangulated-dist-triang

    @joelriou
    joelriou committed Oct 18, 2023
    Configuration menu
    Copy the full SHA
    00fc153 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into pretriangulated-op

    @joelriou
    joelriou committed Oct 18, 2023
    Configuration menu
    Copy the full SHA
    11d641a View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/pretriangulated-dist-triang' int… 

    …o pretriangulated-op
    @joelriou
    joelriou committed Oct 18, 2023
    Configuration menu
    Copy the full SHA
    2a1c6d7 View commit details
    Browse the repository at this point in the history

  4. added a note about the scoped instance for the pretriangulated structure

    @joelriou
    joelriou committed Oct 18, 2023
    Configuration menu
    Copy the full SHA
    7c17e4c View commit details
    Browse the repository at this point in the history