of_injective — Mathlib

English

If N is Noetherian and f: M →ₗ[R] N is injective, then M is finite as an R-module.

Русский

Если N — Noetherian, а f: M →ₗ[R] N инъективно, то M является конечным как R-модуль.

LaTeX

$$$[IsNoetherian R N] \Rightarrow (\text{Injective } f) \Rightarrow Module.Finite R M$$$

Lean4

theorem of_injective [IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective f) : Module.Finite R M :=
  ⟨fg_of_injective f hf⟩

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