[Merged by Bors] - feat: define finite length modules and show equivalence with IsNoetherian ∧ IsArtinian
#17478
+120
−5
IsNoetherian ∧ IsArtinian
#17478