isArtinian_of_linearEquiv — Mathlib

English

If f is a linear equivalence between M and P, and M is Artinian as an R-module, then P is Artinian as an R-module.

Русский

Если f — линейное эквивалентное отображение между M и P, и M артинанов как R-модуль, то и P артинанов как R-модуль.

LaTeX

$$$IsArtinian\\ R\\ M \\Rightarrow IsArtinian\\ R\\ P$$$

Lean4

theorem isArtinian_of_linearEquiv (f : M ≃ₗ[R] P) [IsArtinian R M] : IsArtinian R P :=
  isArtinian_of_surjective _ f.toLinearMap f.toEquiv.surjective

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