isNoetherian_range — Mathlib

English

If a linear map f: M → P is defined, and M is Noetherian, then the range of f is Noetherian.

Русский

Если линейное отображение f: M → P задано, и M является Noetherian, то образ f (range f) является Noetherian.

LaTeX

$$$\forall f: M \to P,\ [IsNoetherian R\ M] \Rightarrow IsNoetherian R\ (\operatorname{range} f)$$$

Lean4

instance isNoetherian_range (f : M →ₗ[R] P) [IsNoetherian R M] : IsNoetherian R (LinearMap.range f) :=
  isNoetherian_of_surjective _ _ f.range_rangeRestrict

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