isNoetherian_span_of_finite — Mathlib

English

In a Noetherian module, a linear independent set spans a finite subfamily.

Русский

В Ноетеровом модуле линейно независимое множество порождает конечное подмножество элементов.

LaTeX

$$$\text{LinearIndependent}(R,v) \Rightarrow Finite(\text{span}(v))$$$

Lean4

/-- In a module over a Noetherian ring, the submodule generated by finitely many vectors is
Noetherian. -/
theorem isNoetherian_span_of_finite (R) {M} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {A : Set M}
    (hA : A.Finite) : IsNoetherian R (Submodule.span R A) :=
  isNoetherian_of_fg_of_noetherian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩)

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