Skip to content

[Merged by Bors] - feat: simple lemmas about fractional ideals#14099

Closed
js2357 wants to merge 6 commits intomasterfrom
js2357/FractionalIdeals
Closed

[Merged by Bors] - feat: simple lemmas about fractional ideals#14099
js2357 wants to merge 6 commits intomasterfrom
js2357/FractionalIdeals

Conversation

@js2357
Copy link
Copy Markdown
Collaborator

@js2357 js2357 commented Jun 24, 2024 •
edited
Loading

Prove five lemmas about fractional ideals (zero_mem, fg_of_isNoetherianRing, den_mem_inv, num_le_mul_inv, bot_lt_mul_inv).

This is part 1/4 of a proof of isDedekindDomain_iff_isDedekindDomainDvr.
Part 2: #14216
Part 3: #14237
Part 4: #14242

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 Jun 24, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 24, 2024 •
edited
Loading

PR summary ffdb237211

Import changes

No significant changes to the import graph

Declarations diff

+ bot_lt_mul_inv
+ den_mem_inv
+ fg_of_isNoetherianRing
+ num_le_mul_inv
+ zero_mem

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 25, 2024

Thanks for your contribution! I presume you're looking for review on your code - I have labelled your pull request awaiting-review to indicate this. You can read more about this label in the contribution guide.

@grunweg grunweg added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jun 25, 2024
@grunweg grunweg changed the title Simple lemmas about fractional ideals feat: simple lemmas about fractional ideals Jun 25, 2024
This was referenced Jun 28, 2024
Closed
Open
Open
erdOne
erdOne approved these changes Jun 30, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 30, 2024
kbuzzard
kbuzzard approved these changes Jun 30, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Thanks a lot for your contribution and I look forward to the future PRs! I've made a suggestion to make one of your proofs perhaps easier to maintain.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 30, 2024

✌️ js2357 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@js2357 @kbuzzard
robustify proof by replacing convert
ffdb237 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@js2357
Copy link
Copy Markdown
Collaborator Author

js2357 commented Jun 30, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@js2357
feat: simple lemmas about fractional ideals (#14099)
c1c6ecd 
Prove five lemmas about fractional ideals (zero_mem, fg_of_isNoetherianRing, den_mem_inv, num_le_mul_inv, bot_lt_mul_inv). 

This is part 1/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`. 
Part 2: #14216
Part 3: #14237
Part 4: #14242
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: simple lemmas about fractional ideals [Merged by Bors] - feat: simple lemmas about fractional ideals Jun 30, 2024
@mathlib-bors mathlib-bors bot closed this Jun 30, 2024
@mathlib-bors mathlib-bors bot deleted the js2357/FractionalIdeals branch June 30, 2024 19:16
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@js2357 @dagurtomas
feat: simple lemmas about fractional ideals (#14099)
ec3538c 
Prove five lemmas about fractional ideals (zero_mem, fg_of_isNoetherianRing, den_mem_inv, num_le_mul_inv, bot_lt_mul_inv). 

This is part 1/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`. 
Part 2: #14216
Part 3: #14237
Part 4: #14242
mathlib-bors bot pushed a commit that referenced this pull request Aug 21, 2024
@js2357
feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions …
559b6a5 
…of fractional ideals (#14216)

Define the extension of a fractional ideal along a ring homomorphism, and prove some basic facts about extensions.

This PR is part 2/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`.
Part 1: #14099
Part 3: #14237
Part 4: #14242

- [x] depends on: #14099
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@js2357 @bjoernkjoshanssen
feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions …
6eb9e55 
…of fractional ideals (#14216)

Define the extension of a fractional ideal along a ring homomorphism, and prove some basic facts about extensions.

This PR is part 2/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`.
Part 1: #14099
Part 3: #14237
Part 4: #14242

- [x] depends on: #14099
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@js2357 @bjoernkjoshanssen
feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions …
a93ebb9 
…of fractional ideals (#14216)

Define the extension of a fractional ideal along a ring homomorphism, and prove some basic facts about extensions.

This PR is part 2/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`.
Part 1: #14099
Part 3: #14237
Part 4: #14242

- [x] depends on: #14099
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@js2357 @bjoernkjoshanssen
feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions …
9b7287a 
…of fractional ideals (#14216)

Define the extension of a fractional ideal along a ring homomorphism, and prove some basic facts about extensions.

This PR is part 2/4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`.
Part 1: #14099
Part 3: #14237
Part 4: #14242

- [x] depends on: #14099
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kbuzzard kbuzzard kbuzzard approved these changes

@erdOne erdOne erdOne approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@js2357 @grunweg @kbuzzard @erdOne