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(Combinatorics/SimpleGraph): define edist and rewrite dist #14582

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat(Combinatorics/SimpleGraph): define edist and rewrite dist #14582

wants to merge 16 commits into from

Commits on Jul 1, 2024

  1. not_reachable_iff_Walk_isEmpty

    @Rida-Hamadani
    Rida-Hamadani committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    0d28e97 View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2024

  1. init

    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    401005c View commit details
    Browse the repository at this point in the history

  2. provide API for dist 

    co-authored-by: Bhavik Mehta <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    353eb9c View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into rida/refactorDist

    @Rida-Hamadani
    Rida-Hamadani authored Jul 9, 2024
    Configuration menu
    Copy the full SHA
    034f3b8 View commit details
    Browse the repository at this point in the history

  4. fixes

    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    1996e74 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. prove iInf_eq_zero

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    ff344f9 View commit details
    Browse the repository at this point in the history

  2. docs and implicit params

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    033d3d9 View commit details
    Browse the repository at this point in the history

  3. remove duplicate

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    aff9421 View commit details
    Browse the repository at this point in the history

  4. use naming convention

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    fa54c4a View commit details
    Browse the repository at this point in the history

  5. Apply suggestions from review. 

    co-authored-by: Kyle Miller <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    0a60d79 View commit details
    Browse the repository at this point in the history

  6. revert unwanted naming changes

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    7024912 View commit details
    Browse the repository at this point in the history

  7. Apply changes from review. 

    co-authered-by: Bhavik Mehta <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    7d8a20b View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

  1. Apply suggestions from review. 

    co-authored-by: Bhavik Mehta
co-authored-by: Kyle Miller
    @Rida-Hamadani
    Rida-Hamadani committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    f59304b View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Combinatorics/SimpleGraph/Metric.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @Rida-Hamadani @github-actions
    Rida-Hamadani and github-actions[bot] authored Jul 11, 2024
    Configuration menu
    Copy the full SHA
    183bcdd View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. fix merge conflict

    @Rida-Hamadani
    Rida-Hamadani committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    4bf5037 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into rida/refactorDist

    @Rida-Hamadani
    Rida-Hamadani authored Jul 22, 2024
    Configuration menu
    Copy the full SHA
    2ebae9c View commit details
    Browse the repository at this point in the history