trivial_lie_zero

Mathlib.Algebra.Lie.Abelian

URI: https://scilib.ai/kg/mathlib#trivial_lie_zero

← MathLib Explorer

English

If a Lie module action is trivial, then [x,m] = 0 for all x in L, m in M.

Русский

Если действие модуля Ли тривиально, то для всех x в L и m в M скобка [x,m] равна 0.

LaTeX

$$∀ x ∈ L, ∀ m ∈ M, [x,m] = 0$$

Lean4

@[simp]
theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [LieModule.IsTrivial L M] (x : L) (m : M) :
    ⁅x, m⁆ = 0 :=
  LieModule.IsTrivial.trivial x m

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru