[Merged by Bors] - feat: define finite length modules and show equivalence with IsNoetherian ∧ IsArtinian
#22466
Loading
IsNoetherian ∧ IsArtinian
#22466