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] - refactor: introduce the new homology API for homological complex and rename the old one #7954

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - refactor: introduce the new homology API for homological complex and rename the old one #7954

wants to merge 11 commits into from

Commits on Oct 26, 2023

  1. wip

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

  2. fixed LeftDerived

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

  3. fixing GroupCohomology.Resolution

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

  4. fixing GroupCohomology.Resolution

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

  5. fixed GroupCohomology.Resolution

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

  6. redefining HomologicalComplex.homology

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

  7. added docstring

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

  8. added docstring

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

  9. removed unnecessary lemmas

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

Commits on Oct 27, 2023

  1. Update Mathlib/Algebra/Homology/Homology.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @joelriou @jcommelin
    joelriou and jcommelin committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    491b4f4 View commit details
    Browse the repository at this point in the history

  2. fixed docstring

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