instLieModule — Mathlib

English

There is a Lie module structure on TrivialLieModule R L (M) given by trivial action; the action maps satisfy the Lie module axioms.

Русский

На тривиальном модуле Ли существует структура модуля Ли, задаваемая тривиальным действием; операции удовлетворяют аксиомам модуля Ли.

LaTeX

$$$\text{LieModule } R\ L\ (TrivialLieModule\ R\ L\ M)$ with \smul_lie and \lie_smul defined by trivial action.$$

Lean4

instance : LieModule R L (TrivialLieModule R L M)
    where
  smul_lie := by simp
  lie_smul := by simp

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