instAddSubgroupClass

Mathlib.Algebra.Lie.Subalgebra

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

← MathLib Explorer

English

A Lie subalgebra is an additive subgroup of its ambient Lie algebra.

Русский

Подалгебра Ли является аддитивной подпоследовательностью пространства.

LaTeX

$$$L'\; \text{is an AddSubgroup of } L$$$

Lean4

instance : AddSubgroupClass (LieSubalgebra R L) L
    where
  add_mem := Submodule.add_mem _
  zero_mem L' := L'.zero_mem'
  neg_mem {L'} x hx := show -x ∈ (L' : Submodule R L) from neg_mem hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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