Documentation

Mathlib.FieldTheory.Finiteness

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

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

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

Equations
Instances For

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

    Equations
    theorem IsNoetherian.finite_basis_index {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} {s : Set ι} [IsNoetherian K V] (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) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :

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

    Equations
    Instances For
      noncomputable def IsNoetherian.finsetBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
      Basis { x : V // x IsNoetherian.finsetBasisIndex K 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
      Instances For

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