traceForm_isSymm

Mathlib.Algebra.Lie.TraceForm

URI: https://scilib.ai/kg/mathlib#LieModule.traceForm_isSymm

English

The trace form is symmetric: traceForm(x,y) = traceForm(y,x) for all x,y ∈ L.

Русский

Trace-form симметрична: traceForm(x,y) = traceForm(y,x) для всех x,y ∈ L.

LaTeX

$$$$ \mathrm{traceForm}(x,y) = \mathrm{traceForm}(y,x). $$$$

Lean4

theorem traceForm_isSymm : LinearMap.IsSymm (traceForm R L M) :=
  ⟨LieModule.traceForm_comm R L M⟩

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

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

Разделы

Аффилиация

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