toEnd

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieRingModule.toEnd

Lean4

/-- The Lie bracket as a biadditive map.

Usually one will have coefficients and `LieModule.toEnd` will be more useful. -/
@[simps]
def toEnd : L →+ M →+ M
    where
  toFun x := ⟨⟨fun m ↦ ⁅x, m⁆, lie_zero x⟩, LieRingModule.lie_add x⟩
  map_zero' := by ext n; exact zero_lie n
  map_add' y z := by ext n; exact add_lie y z n

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

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

Разделы

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

Аффилиация

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