A module over a division ring is noetherian if and only if it is finite. #
A module over a division ring is noetherian if and only if
its dimension (as a cardinal) is strictly less than the first infinite cardinal
In a noetherian module over a division ring, there exists a finite basis.
This is indexed by the
This is in contrast to the result
finite_basis_index (Basis.ofVectorSpace K V),
which provides a set and a