trace_lie

Mathlib.LinearAlgebra.Trace

URI: https://scilib.ai/kg/mathlib#LinearMap.trace_lie

← MathLib Explorer

English

The trace of a Lie bracket [f,g] is zero: tr([f,g]) = 0.

Русский

След скобки Ли [f,g] равен нулю: tr([f,g]) = 0.

LaTeX

$$$\\operatorname{trace}_R M \\,[f,g] = 0$$$

Lean4

@[simp]
theorem trace_lie {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (f g : Module.End R M) :
    trace R M ⁅f, g⁆ = 0 := by
  rw [Ring.lie_def, map_sub, trace_mul_comm]
  exact sub_self _

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

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

Разделы

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

Аффилиация

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