instLieModule — Mathlib

English

There is a Lie module structure on the LieDerivation R L M over L, turning LieDerivation into a Lie L-module.

Русский

Существует структура модуля Ли на пространстве производных, превращающая LieDerivation в модуль Ли над L.

LaTeX

$$instLieModule : LieModule R L (LieDerivation R L M)$$

Lean4

instance instLieModule : LieModule R L (LieDerivation R L M)
    where
  smul_lie t x D := by ext; simp
  lie_smul t x D := by ext; simp

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