restrict_killingForm

Mathlib.Algebra.Lie.TraceForm

URI: https://scilib.ai/kg/mathlib#LieIdeal.restrict_killingForm

English

Under the same hypotheses as 18536, the same containment holds; a simp-variant of the Abelian implication.

Русский

При тех же предпосылках, что и в 18536, выполняется та же вложенность; упрощенная версия следствия абелевости.

LaTeX

$$I ≤ LieIdeal.killingCompl R L ⊤$$

Lean4

theorem restrict_killingForm : (killingForm R L).restrict I = LieModule.traceForm R I L :=
  rfl

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

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

Разделы

Аффилиация

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