instLieModule — Mathlib

English

There is a LieModule structure on LinearMap (RingHom.id R) M R with smul_lie and lie_smul given by the obvious rule.

Русский

Существует структура LieModule на LinearMap (RingHom.id R) M R с действием smul_lie и lie_smul по очевидному правилу.

LaTeX

$$$\text{LieModule } R L (M \to_R R)$ with $smul\_lie$ and $lie\_smul$ defined by $t\cdot x$ rules$$

Lean4

instance instLieModule : LieModule R L (M →ₗ[R] R)
    where
  smul_lie := fun t x m ↦ by ext n; simp
  lie_smul := fun t x m ↦ by ext n; simp

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