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: port RingTheory.Ideal.MinimalPrime #4146

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat: port RingTheory.Ideal.MinimalPrime #4146

wants to merge 23 commits into from

Commits on May 20, 2023

  1. feat: port RingTheory.Ideal.MinimalPrime

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    0a5cedd View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    ce6f32a View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    d007451 View commit details
    Browse the repository at this point in the history

  4. Fix proof

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    ba82f62 View commit details
    Browse the repository at this point in the history

  5. Fix proof

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    1ac3acd View commit details
    Browse the repository at this point in the history

  6. Fix docs

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    f464a72 View commit details
    Browse the repository at this point in the history

  7. Fix name

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    c1925ae View commit details
    Browse the repository at this point in the history

  8. Add missing variable names

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    b941aed View commit details
    Browse the repository at this point in the history

  9. Fix capitalizaion

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    10dcf68 View commit details
    Browse the repository at this point in the history

  10. Add protected

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    64963d6 View commit details
    Browse the repository at this point in the history

  11. Inf -> sInf

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    e4b3097 View commit details
    Browse the repository at this point in the history

  12. Fix proof

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    51664dd View commit details
    Browse the repository at this point in the history

  13. Minor fixes

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    2d5ce2e View commit details
    Browse the repository at this point in the history

  14. Fix linter errors

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    f3e9ba3 View commit details
    Browse the repository at this point in the history

  15. Fix proofs

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    8dc89b3 View commit details
    Browse the repository at this point in the history

  16. Revert unmatched brackets

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    22cdbda View commit details
    Browse the repository at this point in the history

  17. More fixes

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    7857e37 View commit details
    Browse the repository at this point in the history

  18. Fix

    @apurvnakade
    apurvnakade committed May 20, 2023
    Configuration menu
    Copy the full SHA
    11e93a3 View commit details
    Browse the repository at this point in the history

Commits on May 21, 2023

  1. fix Ne, define Localization.isLocalization

    @int-y1
    int-y1 committed May 21, 2023
    Configuration menu
    Copy the full SHA
    b6caefb View commit details
    Browse the repository at this point in the history

  2. fix error with @IsLocalization.map_comp

    @int-y1
    int-y1 committed May 21, 2023
    Configuration menu
    Copy the full SHA
    c7d7030 View commit details
    Browse the repository at this point in the history

  3. fix exists_comap_eq_of_mem_minimalPrimes

    @int-y1
    int-y1 committed May 21, 2023
    Configuration menu
    Copy the full SHA
    5d24586 View commit details
    Browse the repository at this point in the history

  4. golf

    @int-y1
    int-y1 committed May 21, 2023
    Configuration menu
    Copy the full SHA
    f8b2e9a View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into port/RingTheory.Ideal.MinimalPrime

    @apurvnakade
    apurvnakade committed May 21, 2023
    Configuration menu
    Copy the full SHA
    ccd1b70 View commit details
    Browse the repository at this point in the history