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] - chore(AlgebraicTopology/TopologicalSimplex): clean up, golf #9431

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - chore(AlgebraicTopology/TopologicalSimplex): clean up, golf #9431

wants to merge 6 commits into from

Commits on Jan 4, 2024

  1. feat(AlgebraicTopology/SingularSet): factor topology out of `Simplici… 

    …alSet` into new file
    @jcommelin
    jcommelin committed Jan 4, 2024
    Configuration menu
    Copy the full SHA
    724eff2 View commit details
    Browse the repository at this point in the history

  2. fix docs in other file

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

  3. chore(AlgebraicTopology/TopologicalSimplex): clean up, golf

    @jcommelin
    jcommelin committed Jan 4, 2024
    Configuration menu
    Copy the full SHA
    01ada7e View commit details
    Browse the repository at this point in the history

  4. add new file to Mathlib.lean

    @jcommelin
    jcommelin committed Jan 4, 2024
    Configuration menu
    Copy the full SHA
    91fe3df View commit details
    Browse the repository at this point in the history

  5. Merge branch 'singular-set' into top-simplex-cleanup

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

Commits on Jan 5, 2024

  1. no need to depend on other PR

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