traceForm_apply_lie_apply' — Mathlib

English

Re-statement: mapIncl M' N' equals map M'.incl N'.incl, asserting compatibility with submodule inclusions.

Русский

Повтор: mapIncl M' N' = map M'.incl N'.incl, подчёркивая совместимость с включениями подмодулей.

LaTeX

$$$$ \mathrm{mapIncl}(M',N') = \mathrm{map} (M'.\mathrm{incl}, N'.\mathrm{incl}). $$$$

Lean4

/-- Given a representation `M` of a Lie algebra `L`, the action of any `x : L` is skew-adjoint
w.r.t. the trace form. -/
theorem traceForm_apply_lie_apply' (x y z : L) : traceForm R L M ⁅x, y⁆ z = -traceForm R L M y ⁅x, z⁆ :=
  calc
    traceForm R L M ⁅x, y⁆ z = -traceForm R L M ⁅y, x⁆ z := by rw [← lie_skew x y, map_neg, LinearMap.neg_apply]
    _ = -traceForm R L M y ⁅x, z⁆ := by rw [traceForm_apply_lie_apply]

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