instLieRingModule

Mathlib.Algebra.Lie.Abelian

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

Lean4

instance : LieRingModule L (TrivialLieModule R L M)
    where
  bracket x m := 0
  add_lie := by simp
  lie_add := by simp
  leibniz_lie := by simp

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

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

Разделы

Аффилиация

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