instIsNoetherianSubtypeMem

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.instIsNoetherianSubtypeMem

English

If L is Artinian, every Lie subalgebra L' is Artinian.

Русский

Если L - артинь, то любая подалгебра L' тоже артинь.

LaTeX

$$$\text{IsArtinian}(R,L')$ given $\text{IsArtinian}(R,L)$$$

Lean4

instance (L' : LieSubalgebra R L) [IsNoetherian R L] : IsNoetherian R L' :=
  isNoetherian_submodule' _

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

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

Разделы

Аффилиация

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