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

theorem is_noetherian.dim_lt_aleph_0 (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian 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 is_noetherian.fintype_basis_index {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : 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
@[protected, instance]

In a noetherian module over a division ring, basis.of_vector_space is 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] {ι : 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.

noncomputable def is_noetherian.finset_basis_index (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :

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

Equations
noncomputable def is_noetherian.finset_basis (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :

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] :

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