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(Data/Nat/Prime): add 2 theorems #11620

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(Data/Nat/Prime): add 2 theorems #11620

wants to merge 9 commits into from

Commits on Mar 30, 2024

  1. feat(Data/Nat/Prime): add 2 theorems

    @casavaca
    casavaca committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    ae5a55e View commit details
    Browse the repository at this point in the history

  2. fixup: add 2 iff theorems

    @casavaca
    casavaca committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    7be4ead View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Data/Nat/Prime.lean 

    golf from @tb65536

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @casavaca @tb65536
    casavaca and tb65536 committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    ec93200 View commit details
    Browse the repository at this point in the history

  4. Fix rebase

    @casavaca
    casavaca committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    4b9eb09 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

  1. Rename the theorems

    @casavaca
    casavaca committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    fed8b69 View commit details
    Browse the repository at this point in the history

  2. Fix up rename

    @casavaca
    casavaca committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    71f91af View commit details
    Browse the repository at this point in the history

  3. rename the theorem so that the match the actual expr

    @casavaca
    casavaca committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    c87b8a6 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Data/Nat/Prime.lean 

    style

Co-authored-by: damiano <adomani@gmail.com>
    @casavaca @adomani
    casavaca and adomani committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    399921c View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Data/Nat/Prime.lean 

    style

Co-authored-by: damiano <adomani@gmail.com>
    @casavaca @adomani
    casavaca and adomani committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    a41bc51 View commit details
    Browse the repository at this point in the history