instLieRingModule — Mathlib

English

The module A ⊗ M carries a Lie ring module structure over the base Lie ring via the base change of the action and Leibniz rule.

Русский

Модуль A ⊗ M имеет структуру модуля LieRing над базовым LieRing через перенос действия и правило Лейбница.

LaTeX

$$$\text{LieRingModule } (A\otimes_R L) (A\otimes_R M) \text{ with Leibniz_lie}.$$

Lean4

instance instLieRingModule : LieRingModule (A ⊗[R] L) (A ⊗[R] M)
    where
  add_lie x y z := by simp only [bracket_def, LinearMap.add_apply, LinearMap.map_add]
  lie_add x y z := by simp only [bracket_def, LinearMap.map_add]
  leibniz_lie := bracket_leibniz_lie R A L M

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