# Documentation

Mathlib.FieldTheory.Finiteness

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

theorem IsNoetherian.rank_lt_aleph0 (K : Type u) (V : Type v) [] [] [Module K V] [] :

The dimension of a noetherian module over a division ring, as a cardinal, is strictly less than the first infinite cardinal ℵ₀.

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.

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.

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

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.

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 // } = ↑()
noncomputable def IsNoetherian.finsetBasis (K : Type u) (V : Type v) [] [] [Module K V] [] :
Basis { x // } K V

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

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.