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 #
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