instLieAdmissibleRing

Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

URI: https://scilib.ai/kg/mathlib#LeftPreLieRing.instLieAdmissibleRing

Lean4

/-- `LeftPreLieRings` are examples of `LieAdmissibleRings` by the commutatitvity assumption on the
associator. -/
instance instLieAdmissibleRing : LieAdmissibleRing L where
  assoc_def x y
    z := by
    have assoc_xyz := LeftPreLieRing.assoc_symm' x y z
    have assoc_zxy := LeftPreLieRing.assoc_symm' z x y
    have assoc_yzx := LeftPreLieRing.assoc_symm' y z x
    grind

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

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

Разделы

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

Аффилиация

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