Skip to content

[Merged by Bors] - feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals#14216

Closed
js2357 wants to merge 11 commits intomasterfrom
js2357/Extended
Closed

[Merged by Bors] - feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals#14216
js2357 wants to merge 11 commits intomasterfrom
js2357/Extended

Conversation

@js2357
Copy link
Copy Markdown
Collaborator

@js2357 js2357 commented Jun 28, 2024 •
edited
Loading

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

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

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

PR summary 49461bc986

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.FractionalIdeal.Extended 1017

Declarations diff

+ coe_extended_eq_span
+ extended
+ extended_add
+ extended_mul
+ extended_one
+ extended_zero
+ mem_add
+ mem_extended_iff

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

@js2357 js2357 mentioned this pull request Jun 28, 2024
Closed
@js2357 js2357 added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jun 28, 2024
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 28, 2024
This was referenced Jun 28, 2024
Open
Open
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
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 30, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 30, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024
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
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 28, 2024
mattrobball
mattrobball reviewed Aug 19, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball left a comment

Choose a reason for hiding this comment

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

Nice work! Some comments below.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 21, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 21, 2024
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
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 21, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals [Merged by Bors] - feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals Aug 21, 2024
@mathlib-bors mathlib-bors bot closed this Aug 21, 2024
@mathlib-bors mathlib-bors bot deleted the js2357/Extended branch August 21, 2024 12:05
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

@mattrobball mattrobball mattrobball left review comments

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! 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.

3 participants

@js2357 @mattrobball @kim-em