feat(RingTheory/Ideal/Height): prime ideal determined by height among overideals#36789
feat(RingTheory/Ideal/Height): prime ideal determined by height among overideals#36789hommmmm wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 316a0377d0Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
|
||
| /-- A prime ideal of finite height is equal to any ideal of the same height that contains it. -/ | ||
| lemma Ideal.eq_of_le_of_height_eq [I.IsPrime] [I.FiniteHeight] | ||
| (J : Ideal R) (h : I ≤ J) (hIJ : I.height = J.height) : I = J := |
There was a problem hiding this comment.
You can probably generalize this J.height <= I.height?
There was a problem hiding this comment.
I wouldn't keep this around anymore since it's an immediate specialization of the previous.
5 participants
Summary
Ideal.eq_of_le_of_height_eq: a prime ideal of finite height is equal to any ideal of the same height that contains it.Notes
This is a direct consequence of
Ideal.height_strict_mono_of_is_prime: ifIwere strictly contained inJ, their heights would differ.