instLieModule — Mathlib

English

There is a Lie module structure on the direct sum ⨁ i, M i induced by standard componentwise operations.

Русский

На прямой сумме ⨁ i, M_i существует структура модуля Ли, порождаемая по компонентам.

LaTeX

$$DirectSum.instLieModule$$

Lean4

instance : LieModule R L (⨁ i, M i)
    where
  smul_lie t x
    m := by
    ext
    simp only [smul_lie, lie_module_bracket_apply, smul_apply]
  lie_smul t x
    m := by
    ext
    simp only [lie_smul, lie_module_bracket_apply, smul_apply]

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