instLieRing

Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

URI: https://scilib.ai/kg/mathlib#LieAdmissibleRing.instLieRing

Lean4

/-- By definition, every `LieAdmissibleRing` yields a `LieRing` with the commutator bracket. -/
instance instLieRing [LieAdmissibleRing L] : LieRing L
    where
  add_lie x y
    z := by
    simp only [Ring.lie_def, mul_add, add_mul]
    abel
  lie_add x y
    z := by
    simp only [Ring.lie_def, mul_add, add_mul]
    abel
  lie_self := by simp [Ring.lie_def]
  leibniz_lie x y
    z := by
    have := LieAdmissibleRing.assoc_def x y z
    simp only [associator_apply] at this
    grind [Ring.lie_def, mul_sub, sub_mul]

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

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

Разделы

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

Аффилиация

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