lieRing

Mathlib.Algebra.Lie.DirectSum

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

Lean4

instance lieRing : LieRing (⨁ i, L i) :=
  {
    (inferInstance :
      AddCommGroup _) with
    bracket := zipWith (fun _ => fun x y => ⁅x, y⁆) fun _ => lie_zero 0
    add_lie := fun x y z => by
      ext
      simp only [zipWith_apply, add_apply, add_lie]
    lie_add := fun x y z => by
      ext
      simp only [zipWith_apply, add_apply, lie_add]
    lie_self := fun x => by
      ext
      simp only [zipWith_apply, lie_self, zero_apply]
    leibniz_lie := fun x y z => by
      ext
      simp only [zipWith_apply, add_apply]
      apply leibniz_lie }

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

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

Разделы

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

Аффилиация

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