traceForm_lieInvariant — Mathlib

English

The trace form is invariant under the Lie action: for any x ∈ L, the bracket [x, traceForm] vanishes, i.e., traceForm is lie-invariant.

Русский

Trace-form инвариантна относительно действия Ли: для всех x ∈ L скобка [x, traceForm] равна нулю; trace-form инвариантна по Ли.

LaTeX

$$$$ \,[x, \mathrm{traceForm}] = 0. $$$$

Lean4

theorem traceForm_lieInvariant : (traceForm R L M).lieInvariant L :=
  by
  intro x y z
  rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]

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