instLieRingModule — Mathlib

English

The endomorphism algebra Module.End R M acts on M as a Lie module via evaluation, i.e. for f ∈ Module.End R M and m ∈ M, ⁅f, m⁆ = f(m).

Русский

Алгебра линеарных преобразований Module.End R M действует на M как Lie-модуль: ⁅f, m⁆ = f(m).

LaTeX

$$$$[f,m] = f(m) \quad (f \in \mathrm{End}_R(M), \ m \in M).$$$$

Lean4

instance instLieRingModule : LieRingModule (Module.End R M) M :=
  LieRingModule.ofAssociativeModule

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