instNoZeroSMulDivisorsSubtypeMem

Mathlib.Algebra.Lie.Submodule

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

English

The subtype N inherits a LieModule structure over R and L when N is viewed as a subset of M with the bracket action restricted.

Русский

Подтип N наследует структуру LieModule над R и L при ограничении скобочной операции к N.

LaTeX

$$instance (N) : LieModule R L N$$

Lean4

instance [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R N :=
  inferInstanceAs <| NoZeroSMulDivisors R N.toSubmodule

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

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

Разделы

Аффилиация

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