instIsArtinianSubtypeMem

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.instIsArtinianSubtypeMem

English

If R, M satisfy NoZeroSmulDivisors, then the subtype N inherits NoZeroSmulDivisors as an R-module.

Русский

Если R, M удовлетворяют NoZeroSmulDivisors, то подтип N наследует NoZeroSmulDivisors как R-модуль.

LaTeX

$$[NoZeroSMulDivisors R M] ⇒ NoZeroSMulDivisors R N$$

Lean4

instance [IsArtinian R M] (N : LieSubmodule R L M) : IsArtinian R N :=
  inferInstanceAs <| IsArtinian R N.toSubmodule

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

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

Разделы

Аффилиация

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