Commit 2024-10-09 07:18 957d5dd1

feat: define finite length modules and show equivalence with IsNoetherian ∧ IsArtinian (#17478) and equivalence with the existence of a CompositionSeries. Add order-theoretic results: a simple order is finite; WellFoundedLT implies every non-top element is covered by some other element, and the dual result; WellFoundedLT + WellFoundedGT implies there exists a finite sequence from ⊥ to ⊤ with each element covering the previous one. Also generalize two proof_wanted statements about semisimple modules/rings.