isNoetherian_of_isNoetherianRing_of_finite

English

In a Noetherian ring R, a finitely generated submodule N of a module M is Noetherian.

Русский

В кольце Р, которое Ноетерово, подмодуль N модуля M, порождённый конечным множеством элементов, является Ноетеровым.

LaTeX

$$$IsNoetherian(R,N)$ given $N.FG$ and $IsNoetherianRing R$$$

Lean4

instance isNoetherian_of_isNoetherianRing_of_finite (R M : Type*) [Ring R] [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M] : IsNoetherian R M :=
  have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
  isNoetherian_of_surjective _ _ (LinearMap.range_eq_top.mpr h)

Похожие утверждения