instModule — Mathlib

English

For any S, LieDerivation R L M has a natural module structure over S provided SMulCommClass R S M and SMulBracketCommClass S L M; i.e., LieDerivation R L M is a module over S.

Русский

Для любого S производная Ли имеет естественную структуру модуля над S при заданных SMulCommClass R S M и SMulBracketCommClass S L M; т.е. LieDerivation R L M является модулем над S.

LaTeX

$$$\text{Module } S (\text{LieDerivation } R L M)$$$

Lean4

instance instModule {S : Type*} [Semiring S] [Module S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] :
    Module S (LieDerivation R L M) :=
  Function.Injective.module S coeFnAddMonoidHom coe_injective coe_smul

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