# A module over a division ring is noetherian if and only if it is finite. #

theorem IsNoetherian.iff_rank_lt_aleph0 {K : Type u} {V : Type v} [] [] [Module K V] :

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 ℵ₀.

@[deprecated rank_lt_aleph0]
theorem IsNoetherian.rank_lt_aleph0 (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] :

Alias of rank_lt_aleph0.

The rank of a finite module is finite.

noncomputable def IsNoetherian.fintypeBasisIndex {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] (b : Basis ι K V) :

In a noetherian module over a division ring, all bases are indexed by a finite type.

Equations
• = b.fintypeIndexOfRankLtAleph0
Instances For
noncomputable instance IsNoetherian.instFintypeElemOfVectorSpaceIndex {K : Type u} {V : Type v} [] [] [Module K V] [] :

In a noetherian module over a division ring, Basis.ofVectorSpace is indexed by a finite type.

Equations
• IsNoetherian.instFintypeElemOfVectorSpaceIndex =
theorem IsNoetherian.finite_basis_index {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} {s : Set ι} [] (b : Basis (s) K V) :
s.Finite

In a noetherian module over a division ring, if a basis is indexed by a set, that set is finite.

noncomputable def IsNoetherian.finsetBasisIndex (K : Type u) (V : Type v) [] [] [Module K V] [] :

In a noetherian module over a division ring, there exists a finite basis. This is the indexing Finset.

Equations
• = .toFinset
Instances For
@[simp]
theorem IsNoetherian.coe_finsetBasisIndex (K : Type u) (V : Type v) [] [] [Module K V] [] :
@[simp]
theorem IsNoetherian.coeSort_finsetBasisIndex (K : Type u) (V : Type v) [] [] [Module K V] [] :
{ x : V // } = ()
noncomputable def IsNoetherian.finsetBasis (K : Type u) (V : Type v) [] [] [Module K V] [] :
Basis { x : V // } K V

In a noetherian module over a division ring, there exists a finite basis. This is indexed by the Finset IsNoetherian.finsetBasisIndex. This is in contrast to the result finite_basis_index (Basis.ofVectorSpace K V), which provides a set and a Set.finite.

Equations
• = ().reindex (.mpr ())
Instances For
@[simp]
theorem IsNoetherian.range_finsetBasis (K : Type u) (V : Type v) [] [] [Module K V] [] :
theorem IsNoetherian.iff_fg {K : Type u} {V : Type v} [] [] [Module K V] :

A module over a division ring is noetherian if and only if it is finitely generated.