finitePresentation_of_finite — Mathlib

English

If R is Noetherian and M is a finitely generated R-module, then M is finitely presented over R.

Русский

Если R Ноетерова, и M — конечно порожденный R-модуль, то M является конечнопредставимым над R.

LaTeX

$$$[IsNoetherianRing\ R]\; [Module.Finite R M] \Rightarrow Module.FinitePresentation R M$$$

Lean4

theorem finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] : Module.FinitePresentation R M :=
  by
  obtain ⟨s, hs⟩ := h
  exact ⟨s, hs, IsNoetherian.noetherian _⟩

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