isArtinian_span_of_finite — Mathlib

English

In a module over an Artinian ring, the submodule generated by a finite set of vectors is Artinian.

Русский

В модуле над артинановым кольцом подмодуль, порожденный конечным множеством векторов, артинанов.

LaTeX

$$$ IsArtinianRing\\; R \\Rightarrow \\forall A\\; A\\text{ finite} \\Rightarrow IsArtinianR(Submodule.span\\; R\\ A). $$$

Lean4

/-- In a module over an Artinian ring, the submodule generated by finitely many vectors is
Artinian. -/
theorem isArtinian_span_of_finite (R) {M} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] {A : Set M}
    (hA : A.Finite) : IsArtinian R (Submodule.span R A) :=
  isArtinian_of_fg_of_artinian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩)

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