PR summary 2bb78d082e

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

This PR/issue depends on:

• [Merged by Bors] - feat: Noetherian/Artinian is closed under extensions (submodule form) #17425
  By Dependent Issues (🤖). Happy coding!

Thanks 🎉

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

Firstly thank you for doing this work, I'm really glad that we now have these results.

However since I was whining about this on Zulip I thought I might outline the API that I would have preferred. Instead of having the definition IsFiniteLength and its API, we would have the following two results (and whatever was required to support them):

theorem isNoetherian_and_isArtinian_iff_exists_compositionSeries :
    IsNoetherian R M ∧ IsArtinian R M ↔
    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by
  sorry

theorem isNoetherian_and_isArtinian_iff_exists_submodule :
    IsNoetherian R M ∧ IsArtinian R M ↔
    Subsingleton M ∨
    ∃ p : Submodule R M, IsSimpleModule R (M ⧸ p) ∧ IsNoetherian R p ∧ IsArtinian R p := by
  sorry

I have just too many draws on my time at the moment to make PR with this refactor but I think it should be easy given what you've already done ;-)

Hi, thanks for the feedback! My main purpose of making an inductive definition IsFiniteLength is to get the nice induction principle, which is used to prove noether/artinianity. This was also my answer to Kevin's questioning about the definition on Zulip. If you define IsFiniteLength using CompositionSeries, you can still prove the same induction principle using an induction similar to my proof of isFiniteLength_of_exists_compositionSeries, but why not get it directly if you can.