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(Algebra/Homology): the mapping cone #8951

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat(Algebra/Homology): the mapping cone #8951

wants to merge 23 commits into from

Commits on Dec 10, 2023

  1. feat(Algebra/Homology): the mapping cone

    @joelriou
    joelriou committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    1cb3659 View commit details
    Browse the repository at this point in the history

  2. generalized the definition

    @joelriou
    joelriou committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    07d8532 View commit details
    Browse the repository at this point in the history

  3. renamed the file

    @joelriou
    joelriou committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    5fbb7f5 View commit details
    Browse the repository at this point in the history

  4. fixed most sorries

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

  5. fixing Mathlib.lean

    @joelriou
    joelriou committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    9f70e44 View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2023

  1. cleaning up

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

  2. removed parentheses

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

  3. definitions for the mapping cone

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

  4. more API for the mapping cone

    @joelriou
    joelriou committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    6611c61 View commit details
    Browse the repository at this point in the history

  5. descHomotopy, liftCochain

    @joelriou
    joelriou committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    6e7ea7c View commit details
    Browse the repository at this point in the history

  6. finished basic API for mapping cone

    @joelriou
    joelriou committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    7830e4d View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2023

  1. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    9910aa1 View commit details
    Browse the repository at this point in the history

Commits on Dec 27, 2023

  1. Merge remote-tracking branch 'origin' into mapping-cone

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

Commits on Jan 2, 2024

  1. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 2, 2024
    Configuration menu
    Copy the full SHA
    7a55841 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 2, 2024
    Configuration menu
    Copy the full SHA
    4becbc1 View commit details
    Browse the repository at this point in the history

  3. fixed the build

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

Commits on Jan 5, 2024

  1. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    4d870ae View commit details
    Browse the repository at this point in the history

  2. fixing the build

    @joelriou
    joelriou committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    fd801a5 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2024

  1. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    1606caf View commit details
    Browse the repository at this point in the history

  2. cleaning up

    @joelriou
    joelriou committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    8aed216 View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2024

  1. Merge remote-tracking branch 'origin' into mapping-cone

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

Commits on Jan 9, 2024

  1. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    68abe94 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into mapping-cone

    @joelriou
    joelriou committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    d605bfa View commit details
    Browse the repository at this point in the history