instSMulMemClass

Mathlib.Algebra.Lie.Subalgebra

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

English

A Lie subalgebra inherits an R-module structure from the ambient Lie algebra.

Русский

Подалгебра наследует структуру модуля над R от всей Ли-алгебры.

LaTeX

$$$L' \text{ is an } R\text{-module with respect to } L$$$

Lean4

instance : SMulMemClass (LieSubalgebra R L) R L where smul_mem {s} := SMulMemClass.smul_mem (s := s.toSubmodule)

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

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

Разделы

Аффилиация

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