isArtinian_of_fg_of_artinian — Mathlib

English

If N ≤ M is finitely generated as an R-submodule of an Artinian ring R, then N is Artinian.

Русский

Если N ≤ M и N порожден конечным числом, то N артинаново.

LaTeX

$$$ [IsArtinianRing\\; R] \\Rightarrow [N.FG] \\Rightarrow IsArtinianR N. $$$

Lean4

theorem isArtinian_of_fg_of_artinian {R M} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsArtinianRing R]
    (hN : N.FG) : IsArtinian R N := by rw [← Module.Finite.iff_fg] at hN; infer_instance

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