isArtinian_range — Mathlib

English

If f is a linear map M →ₗ[R] P and M is Artinian as an R-module, then the range of f is Artinian as an R-module.

Русский

Пусть f: M →ₗ[R] P. Если M артинанов как R-модуль, то образ f (range f) артинанов как R-модуль.

LaTeX

$$$IsArtinian\\ R\\ M \\Rightarrow IsArtinian\\ R\\ (LinearMap.range\\ f)$$$

Lean4

instance isArtinian_range (f : M →ₗ[R] P) [IsArtinian R M] : IsArtinian R (LinearMap.range f) :=
  isArtinian_of_surjective _ _ f.surjective_rangeRestrict

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