feat(RingTheory/Localization): Nagata's criterion for primality in localization away#36785
feat(RingTheory/Localization): Nagata's criterion for primality in localization away#36785hommmmm wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
This is a new fork of mathlib 4 for PR. Original edits were made in https://github.com/uw-math-ai/auslander-buchsbaum
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
|
|
Welcome! Could you please clarify if and how you used AI for (parts of) this pull request? Note that our contribution guidelines require disclosure of any AI assistance. |
chrisflav
added
the
awaiting-author
Updated PR message with AI disclosure -awaiting-author |
github-actions
bot
removed
the
awaiting-author
2 participants
Summary
dvd_of_mem_span_singleton_localization: ifpis prime andp ∤ x, thenmembership in the span of the image of
xinR[1/p]implies divisibility byx.prime_of_prime_in_localization(Nagata's criterion): ifpis prime,xisirreducible, and the image of
xinR[1/p]is prime, thenxis prime.References
AI Disclosure
This code is written without AI, then uses Claude Code with cameronfreer's Lean4-skills (specifically, the
review,refactor, andgolfworkflow) for style changes, refactoring and golfing.