finitePresentation_iff_finite — Mathlib

English

Over a Noetherian ring R, a module M is finitely presented if and only if it is finitely generated.

Русский

Над кольцом Ноetherian модуль M является конечнопредставимым тогда и только тогда, когда он конечно порожден.

LaTeX

$$$[IsNoetherianRing\ R] \Rightarrow (Module.FinitePresentation R M \iff Module.Finite R M)$$$

Lean4

theorem finitePresentation_iff_finite [IsNoetherianRing R] : Module.FinitePresentation R M ↔ Module.Finite R M :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ finitePresentation_of_finite R M⟩

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