Noetherian modules and finiteness of chains

Main results

Let R be a ring and let M be an R-module.

• eventuallyConst_of_isNoetherian: an ascending chain of submodules in a Noetherian module is eventually constant

References

• M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra
• P. Samuel, Algebraic Theory of Numbers

Tags

Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module

theorem eventuallyConst_of_isNoetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : ℕ →o Submodule R M) : Filter.EventuallyConst (⇑f) Filter.atTop