# mathlib3documentation

field_theory.finiteness

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem is_noetherian.iff_rank_lt_aleph_0 {K : Type u} {V : Type v} [ 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 is_noetherian.rank_lt_aleph_0 (K : Type u) (V : Type v) [ V] [ 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} [ V] {ι : Type u_1} [ V] (b : K V) :

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

Equations
@[protected, instance]
noncomputable def is_noetherian.basis.of_vector_space_index.fintype {K : Type u} {V : Type v} [ V] [ V] :

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} [ V] {ι : Type u_1} {s : set ι} [ V] (b : 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) [ V] [ V] :

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

Equations
@[simp]
theorem is_noetherian.coe_finset_basis_index (K : Type u) (V : Type v) [ V] [ V] :
@[simp]
theorem is_noetherian.coe_sort_finset_basis_index (K : Type u) (V : Type v) [ V] [ V] :
noncomputable def is_noetherian.finset_basis (K : Type u) (V : Type v) [ V] [ V] :
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
@[simp]
theorem is_noetherian.range_finset_basis (K : Type u) (V : Type v) [ V] [ V] :
theorem is_noetherian.iff_fg {K : Type u} {V : Type v} [ V] :

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