set_finite_of_isNoetherian — Mathlib

English

If a subset s of a Noetherian module M is linearly independent (via the inclusion map s → M), then s is finite.

Русский

Если подмножество s модуля M является линейно независимым через включение s → M, то оно конечно.

LaTeX

$$$s$ является конечным: $s \text{ finite}$$$

Lean4

theorem set_finite_of_isNoetherian [Nontrivial R] {s : Set M} (hi : LinearIndependent R ((↑) : s → M)) : s.Finite :=
  @Set.toFinite _ _ hi.finite_of_isNoetherian

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