mathlib documentation

field_theory.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 omega.

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

def is_noetherian.fintype_basis_index {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [is_noetherian_ring K] {ι : Type u_1} [is_noetherian K V] (b : basis ι K V) :

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

Equations
theorem is_noetherian.finite_basis_index {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [is_noetherian_ring K] {ι : Type u_1} {s : set ι} [is_noetherian K V] (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.

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

Equations

In a noetherian module over a division ring, there exists a finite basis. This is indexed by the finset finite_dimensional.finset_basis_index. This is in contrast to the result finite_basis_index (basis.of_vector_space K V), which provides a set and a set.finite.

Equations
theorem is_noetherian.iff_fg {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [is_noetherian_ring K] :

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