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

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Dec 15, 2023 •
edited

Co-PR: #9088 (minimal prime ideals in Noetherian ring are finite)

Open in Gitpod

@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR awaiting-CI t-algebra Algebra (groups, rings, fields etc) labels Dec 15, 2023
@jjaassoonn jjaassoonn mentioned this pull request Dec 15, 2023
Draft
1 task
@jjaassoonn jjaassoonn mentioned this pull request Dec 15, 2023
Closed
alreadydone
alreadydone reviewed Dec 15, 2023
View reviewed changes
Copy link
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

Mathlib/RingTheory/Artinian.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Artinian.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Artinian.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Ideal/Operations.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Ideal/Operations.lean Outdated Show resolved Hide resolved
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 17, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 19, 2023
alreadydone
alreadydone approved these changes Dec 19, 2023
View reviewed changes
Mathlib/RingTheory/Artinian.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Artinian.lean Outdated Show resolved Hide resolved
jjaassoonn and others added 2 commits December 20, 2023 12:56
@jjaassoonn
add iff
b9f62b9
@jjaassoonn @alreadydone
Update Mathlib/RingTheory/Artinian.lean
14cd01e 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jjaassoonn @alreadydone
更新 Artinian.lean
30308a1 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
alreadydone
alreadydone approved these changes Dec 20, 2023
View reviewed changes
Copy link
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maintainer merge

Mathlib/RingTheory/Artinian.lean
/--
[Stacks Lemma 00J7](https://stacks.math.columbia.edu/tag/00J7)
-/
lemma maximal_ideals_finite : {I : Ideal R | I.IsMaximal}.Finite := by
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd personally name it as setOf_isMaximal_finite but I think this is also acceptable.

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by alreadydone.

1 similar comment
@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by alreadydone.

jcommelin
jcommelin approved these changes Dec 20, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Dec 20, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 20, 2023
@jjaassoonn
feat(RingTheory/Artinian): the collection of maximal ideals in an art…
9643670 
…inian ring is finite (#9087)

Co-PR: #9088 (minimal prime ideals in Noetherian ring are finite)
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 20, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/Artinian): the collection of maximal ideals in an artinian ring is finite [Merged by Bors] - feat(RingTheory/Artinian): the collection of maximal ideals in an artinian ring is finite Dec 20, 2023
@mathlib-bors mathlib-bors bot closed this Dec 20, 2023
@mathlib-bors mathlib-bors bot deleted the zjj/ArtinianRing-maximalIdeals-finite branch December 20, 2023 20:21
mathlib-bors bot pushed a commit that referenced this pull request Jan 1, 2024
@jjaassoonn @alreadydone
feat(AlgebraicGeometry/PrimeSpectrum/*) : the collection of minimal p…
f3a2680 
…rime ideals of a Noetherian ring is finite (#9088)

Co-PR :  #9087 (maximal ideals of Artinian ring are finite)

Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone approved these changes

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@jjaassoonn @alreadydone @jcommelin @leanprover-community-mathlib4-bot