lie_traceForm_eq_zero — Mathlib

English

For x ∈ L, the bracket [x, traceForm] is the zero bilinear form on M; i.e., traceForm is skew-symmetric with respect to x.

Русский

Для x ∈ L скобка [x, traceForm] равна нулевой билинейной форме на M; trace-form скользит по Ли-основному.

LaTeX

$$$$ [x, \\mathrm{traceForm}] = 0 \,\,\\text{for all } x \\in L. $$$$

Lean4

/-- This lemma justifies the terminology "invariant" for trace forms. -/
@[simp]
theorem lie_traceForm_eq_zero (x : L) : ⁅x, traceForm R L M⁆ = 0 :=
  by
  ext y z
  rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply, LinearMap.zero_apply,
    traceForm_apply_lie_apply', sub_self]

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