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(RingTheory/Artinian): the collection of maximal ideals in an artinian ring is finite #9087

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(RingTheory/Artinian): the collection of maximal ideals in an artinian ring is finite #9087

wants to merge 11 commits into from

Commits on Dec 15, 2023

  1. feat(RingTheory/Artinian): the collection of maximal ideals in an art… 

    …inian ring is finite
    @jjaassoonn
    jjaassoonn committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    bebdcb8 View commit details
    Browse the repository at this point in the history

  2. add comments

    @jjaassoonn
    jjaassoonn committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    ed4b287 View commit details
    Browse the repository at this point in the history

  3. fix doc

    @jjaassoonn
    jjaassoonn committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    6c003ff View commit details
    Browse the repository at this point in the history

  4. Update Artinian.lean

    @jjaassoonn
    jjaassoonn committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    773d1f4 View commit details
    Browse the repository at this point in the history

  5. use approach outlined by @alreadyone

    @jjaassoonn
    jjaassoonn committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    e9e94d6 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2023

  1. Merge remote-tracking branch 'origin/master' into zjj/ArtinianRing-ma… 

    …ximalIdeals-finite
    @jjaassoonn
    jjaassoonn committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    322e9d4 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
    @jjaassoonn @alreadydone
    jjaassoonn and alreadydone committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    53e2b0e View commit details
    Browse the repository at this point in the history

  3. fix

    @jjaassoonn
    jjaassoonn committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    1165c70 View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2023

  1. add iff

    @jjaassoonn
    jjaassoonn committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    b9f62b9 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/RingTheory/Artinian.lean 

    Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
    @jjaassoonn @alreadydone
    jjaassoonn and alreadydone committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    14cd01e View commit details
    Browse the repository at this point in the history

  3. 更新 Artinian.lean 

    Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
    @jjaassoonn @alreadydone
    jjaassoonn and alreadydone committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    30308a1 View commit details
    Browse the repository at this point in the history