instLieRingModule

Mathlib.Algebra.Lie.DirectSum

URI: https://scilib.ai/kg/mathlib#DirectSum.instLieRingModule

Lean4

instance : LieRingModule L (⨁ i, M i)
    where
  bracket x m := m.mapRange (fun _ m' => ⁅x, m'⁆) fun _ => lie_zero x
  add_lie x y
    m := by
    ext
    simp only [mapRange_apply, add_apply, add_lie]
  lie_add x m
    n := by
    ext
    simp only [mapRange_apply, add_apply, lie_add]
  leibniz_lie x y
    m := by
    ext
    simp only [mapRange_apply, lie_lie, add_apply, sub_add_cancel]

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

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

Разделы

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

Аффилиация

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