isArtinian_of_fg_of_artinian' — Mathlib

English

If R is Artinian and M is a finitely generated R-module, then M is Artinian.

Русский

Если R артинаново и M — конечнопорождённый R-модуль, то M артинанов.

LaTeX

$$$ [IsArtinianRing\\; R] \\Rightarrow [Module.Finite\\; R\\; M] \\Rightarrow IsArtinianR M. $$$

Lean4

instance isArtinian_of_fg_of_artinian' {R M} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R]
    [Module.Finite R M] : IsArtinian R M :=
  have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
  isArtinian_of_surjective _ _ h

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