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][atiyah-macdonald]
- [samuel1967]
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