Skip to content

[Merged by Bors] - Chore: Weaken hypotheses for proof that Noetherian is an extension property#12453

Closed
Shamrock-Frost wants to merge 5 commits intomasterfrom
noetherian_of_exact_sequence
Closed

[Merged by Bors] - Chore: Weaken hypotheses for proof that Noetherian is an extension property#12453
Shamrock-Frost wants to merge 5 commits intomasterfrom
noetherian_of_exact_sequence

Conversation

@Shamrock-Frost
Copy link
Copy Markdown
Contributor

@Shamrock-Frost Shamrock-Frost commented Apr 26, 2024

The middle term of a three term exact sequence with outer terms Noetherian is Noetherian.

Open in Gitpod

@Shamrock-Frost Shamrock-Frost added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Apr 26, 2024
erdOne
erdOne reviewed Apr 26, 2024
View reviewed changes
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Apr 26, 2024

Also please start the PR title with feat: or chore: etc. See https://leanprover-community.github.io/contribute/commit.html for details.

@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 26, 2024
@Shamrock-Frost Shamrock-Frost changed the title Weaken hypotheses for proof that Noetherian is an extension property Chore: Weaken hypotheses for proof that Noetherian is an extension property Apr 26, 2024
@Shamrock-Frost Shamrock-Frost added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 26, 2024
@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 26, 2024
github-actions[bot]
github-actions bot reviewed Apr 26, 2024
View reviewed changes
@Shamrock-Frost Shamrock-Frost added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 26, 2024
@Shamrock-Frost @github-actions
Satisfy linter again
742800e 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Apr 26, 2024

Kind reminder: this still fails CI

@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 26, 2024
@Shamrock-Frost
Copy link
Copy Markdown
Contributor Author

Shamrock-Frost commented Apr 26, 2024

Sorry, I was headed into a movie and trying to get the PR fixed on my phone before it started (I did not succeed).

@Shamrock-Frost Shamrock-Frost added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 26, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Apr 27, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 27, 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 Apr 27, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Apr 27, 2024

No worries. Thanks for the contribution!

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Apr 27, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 27, 2024
@Shamrock-Frost
Chore: Weaken hypotheses for proof that Noetherian is an extension pr…
33a5bed 
…operty (#12453)

The middle term of a three term exact sequence with outer terms Noetherian is Noetherian.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title Chore: Weaken hypotheses for proof that Noetherian is an extension property [Merged by Bors] - Chore: Weaken hypotheses for proof that Noetherian is an extension property Apr 27, 2024
@mathlib-bors mathlib-bors bot closed this Apr 27, 2024
@mathlib-bors mathlib-bors bot deleted the noetherian_of_exact_sequence branch April 27, 2024 07:15
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@Shamrock-Frost @apnelson1
Chore: Weaken hypotheses for proof that Noetherian is an extension pr…
6e67368 
…operty (#12453)

The middle term of a three term exact sequence with outer terms Noetherian is Noetherian.
callesonne pushed a commit that referenced this pull request May 16, 2024
@Shamrock-Frost @callesonne
Chore: Weaken hypotheses for proof that Noetherian is an extension pr…
422764b 
…operty (#12453)

The middle term of a three term exact sequence with outer terms Noetherian is Noetherian.
@alreadydone alreadydone mentioned this pull request Oct 4, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Oct 7, 2024
@alreadydone
feat: Noetherian/Artinian is closed under extensions (submodule form) (…
9383423 
…#17425)

+ Add `isNoetherian/Artinian_iff_submodule_quotient`.

+ Remove unnecessary assumptions from `isArtinian_of_range_eq_ker`, mimicking #12453.

+ Move up two instances `isArtinian_of_quotient_of_artinian` and `isNoetherian_of_finite`.

+ Golf `isNoetherian/Artinian_pi`.
mathlib-bors bot pushed a commit that referenced this pull request Oct 7, 2024
@alreadydone
feat: Noetherian/Artinian is closed under extensions (submodule form) (…
4d57c2c 
…#17425)

+ Add `isNoetherian/Artinian_iff_submodule_quotient`.

+ Remove unnecessary assumptions from `isArtinian_of_range_eq_ker`, mimicking #12453.

+ Move up two instances `isArtinian_of_quotient_of_artinian` and `isNoetherian_of_finite`.

+ Golf `isNoetherian/Artinian_pi`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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

@Shamrock-Frost @erdOne @riccardobrasca