instLieModule — Mathlib

English

The Lie module structure on the base-changed tensor product A ⊗ M is compatible with the action of A and R, making it a LieModule over A.

Русский

Структура модуля Ли на A ⊗ M совместима с действием A и R, образуя модуль Ли над A.

LaTeX

$$$\text{LieModule } A (A\otimes_R L) (A\otimes_R M)\text{ with baseChange compatibility}$$$

Lean4

instance instLieModule : LieModule A (A ⊗[R] L) (A ⊗[R] M)
    where
  smul_lie t x m := by simp only [bracket_def, map_smul, LinearMap.smul_apply]
  lie_smul _ _ _ := map_smul _ _ _

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