isArtinian_submodule'

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#isArtinian_submodule'

English

If M is Artinian over R and N is a submodule, then N is Artinian over R.

Русский

Если M артин, то любой подмодуль N тоже артин над R.

LaTeX

$$$\\mathrm{IsArtinian}_R(M) \\Rightarrow \\mathrm{IsArtinian}_R(N)$ for any submodule N ≤ M.$$

Lean4

instance isArtinian_submodule' [IsArtinian R M] (N : Submodule R M) : IsArtinian R N :=
  isArtinian_of_injective N.subtype Subtype.val_injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru