fg_of_injective — Mathlib

English

Let N be a submodule of M. If P is Noetherian and there is an injective linear map M → P, then N is finitely generated.

Русский

Пусть N — подмодуль M. Если P — Noetherian и существует инъективное линейное отображение M → P, то N выпукло порожден.

LaTeX

$$$[IsNoetherian R P] \to (\exists f: M \to P, \text{Injective } f) \Rightarrow N.FG$$$

Lean4

theorem fg_of_injective [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : Function.Injective f) : N.FG :=
  haveI := isNoetherian_of_injective f hf
  IsNoetherian.noetherian N

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