finite_def — Mathlib

English

Let M be an R-module. Then M is finitely generated as an R-module if and only if the top submodule ⊤ of M is finitely generated.

Русский

Пусть M — R-модуль. Тогда M конечно порождается как R-модуль тогда и только тогда, когда верхний подмодуль ⊤ M FG.

LaTeX

$$$\text{Module.Finite } R M \iff (\top : \text{Submodule } R M).FG$$$

Lean4

theorem finite_def {R M} [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R M ↔ (⊤ : Submodule R M).FG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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