fg_of_ker_bot — Mathlib

English

If f: M →ₗ[R] N has trivial kernel, then M is Noetherian if N is Noetherian.

Русский

Если у линейного отображения f: M →ₗ[R] N тривиальное ядро, и N Noetherian, то M тоже Noetherian.

LaTeX

$$$[IsNoetherian R N] \wedge (\ker f = 0) \Rightarrow IsNoetherian R M$$$

Lean4

theorem fg_of_ker_bot [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : N.FG :=
  haveI := isNoetherian_of_ker_bot f hf
  IsNoetherian.noetherian N

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