isNoetherian_of_ker_bot — Mathlib

English

If the first and last modules in an exact sequence are Noetherian, then the middle module is Noetherian.

Русский

Если первая и последняя модули в точной последовательности — Noetherian, то и средняя модуль — Noetherian.

LaTeX

$$$[IsNoetherian R M] \wedge [IsNoetherian R P]\Rightarrow IsNoetherian R N$$

Lean4

theorem isNoetherian_of_ker_bot [IsNoetherian R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : IsNoetherian R M :=
  isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f <| LinearMap.ker_eq_bot.mp hf).symm

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