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(Probability/Kernel/CondCdf): cleanup #10635

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - chore(Probability/Kernel/CondCdf): cleanup #10635

wants to merge 17 commits into from

Commits on Feb 16, 2024

  1. feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]...

    @mo271
    mo271 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    c742eb4 View commit details
    Browse the repository at this point in the history

  2. review comments

    @mo271
    mo271 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    d671f67 View commit details
    Browse the repository at this point in the history

  3. rename

    @mo271
    mo271 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    dd3f397 View commit details
    Browse the repository at this point in the history

  4. chore(Probability/Kernel/CondCdf): cleanup

    @mo271
    mo271 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    e2550a2 View commit details
    Browse the repository at this point in the history

  5. lint

    @mo271
    mo271 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    87ad462 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2024

  1. Merge branch 'master' into mo271/notBddAbove_coe

    @mo271
    mo271 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    6acca14 View commit details
    Browse the repository at this point in the history

  2. fix after merge

    @mo271
    mo271 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    ad1619d View commit details
    Browse the repository at this point in the history

  3. don't repeat proofs

    @mo271
    mo271 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    aa2b779 View commit details
    Browse the repository at this point in the history

  4. fix build

    @mo271
    mo271 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    a097883 View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2024

  1. Update Mathlib/Data/Real/Archimedean.lean 

    Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
    @mo271 @RemyDegenne
    mo271 and RemyDegenne committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    9e14988 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Data/Real/Archimedean.lean 

    Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
    @mo271 @RemyDegenne
    mo271 and RemyDegenne committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    2ca8371 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Data/Real/Archimedean.lean 

    Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
    @mo271 @RemyDegenne
    mo271 and RemyDegenne committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    98812da View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Data/Real/Archimedean.lean

    @mo271
    mo271 committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    4e87d94 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Data/Real/Archimedean.lean

    @mo271
    mo271 committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    7717d03 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Data/Real/Archimedean.lean

    @mo271
    mo271 committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    6e7896d View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Data/Real/Archimedean.lean

    @mo271
    mo271 committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    7856cae View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Data/Real/Archimedean.lean 

    Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
    @mo271 @RemyDegenne
    mo271 and RemyDegenne committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    97e5790 View commit details
    Browse the repository at this point in the history