Theorems · Theorem · ring theory

isNoetherian_of_finite_isArtinian

∀ (M : Type u) [inst : AddCommGroup M] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  [IsArtinian R M], IsNoetherian R M

A finitely generated Artinian module over a commutative ring is Noetherian. This is not necessarily the case over a noncommutative ring, see https://mathoverflow.net/a/61700.

Defined in

Mathlib.RingTheory.HopkinsLevitzki

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupCommRingModuleModule.FiniteIsArtinian