FG — Mathlib · SciLib

English

A submodule N of M is finitely generated if it is the span of a finite subset of M.

Русский

Подмодуль N подмодуля M финитно порождается, если он равен span от конечного множества элементов M.

LaTeX

$$$N.FG \iff \exists S \subseteq M, S \text{ finite } \wedge \operatorname{span}_R S = N.$$$

Lean4

/-- A submodule of `M` is finitely generated if it is the span of a finite subset of `M`. -/
def FG (N : Submodule R M) : Prop :=
  ∃ S : Finset M, Submodule.span R ↑S = N

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