instCoeLieSubalgebraSubmodule

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#instCoeLieSubalgebraSubmodule

English

Every Lie subalgebra is a submodule of the underlying Lie algebra.

Русский

Каждая подалгебра Ли является подмодулем соответствующей Ли-алгебры.

LaTeX

$$$L' \text{ is a } R\text{-submodule of } L$.$$

Lean4

instance : Coe (LieSubalgebra R L) (Submodule R L) :=
  ⟨LieSubalgebra.toSubmodule⟩

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

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

Разделы

Аффилиация

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