Skip to content

feat(RingTheory): height of span of a prime element is one#36788

Open
hommmmm wants to merge 4 commits intoleanprover-community:masterfrom
hommmmm:height-one-of-prime-ele
Open

feat(RingTheory): height of span of a prime element is one#36788
hommmmm wants to merge 4 commits intoleanprover-community:masterfrom
hommmmm:height-one-of-prime-ele

Conversation

@hommmmm
Copy link
Copy Markdown

@hommmmm hommmmm commented Mar 18, 2026

Summary

  • Add Ideal.height_span_singleton_eq_one_of_prime: in a Noetherian integral domain, the ideal generated by a prime element has height one.

Notes

The new theorem follows directly from height_le_one_of_isPrincipal_of_mem_minimalPrimes (upper bound) and the fact that span {p} ≠ ⊥ for p prime (lower bound).

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 18, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 18, 2026

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 awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

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.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 18, 2026 •
edited
Loading

PR summary 92859b95b8

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Ideal.height_span_singleton

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 scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-ring-theory Ring theory label Mar 18, 2026
Multramate
Multramate approved these changes Mar 31, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@Multramate Multramate left a comment

Choose a reason for hiding this comment

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

LGTM! Thanks :)

@Multramate
Copy link
Copy Markdown
Collaborator

Multramate commented Mar 31, 2026

While you're here, note that Ideal.height_le_spanRank_toENat_of_mem_minimal_primes should be named Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes instead, and the module docstring for this and for Ideal.height_le_iff_exists_minimalPrimes should be fixed, but these should be in a separate PR.

hommmmm and others added 2 commits March 31, 2026 11:59
@hommmmm @Multramate
Proof style update
94df4b0 
Changed finishing simp only to simp_rw

Co-authored-by: David Kurniadi Angdinata <[email protected]>
@hommmmm
Fix long line
bbfc91f
@hommmmm hommmmm force-pushed the height-one-of-prime-ele branch 2 times, most recently from f88b87e to bbfc91f Compare March 31, 2026 21:48
@hommmmm
Copy link
Copy Markdown
Author

hommmmm commented Mar 31, 2026

While you're here, note that Ideal.height_le_spanRank_toENat_of_mem_minimal_primes should be named Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes instead, and the module docstring for this and for Ideal.height_le_iff_exists_minimalPrimes should be fixed, but these should be in a separate PR.

Thanks and fixed. See #37463.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@Multramate Multramate Multramate approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@mattrobball mattrobball

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hommmmm @Multramate @mattrobball