traceForm_eq_zero_of_isNilpotent — Mathlib

English

If the Lie algebra L acts nilpotently on M (and the representation is finite/free), then the trace form vanishes identically.

Русский

Если действие Ли-алгебры L на M является никелепным (и представление конечно свободно), то trace-form тождественно равно нулю.

LaTeX

$$$$ \\mathrm{traceForm}(R,L,M) = 0 \quad\\text{when } L \\text{ acts nilpotently on } M.$$$$

Lean4

@[simp]
theorem traceForm_eq_zero_of_isNilpotent [IsReduced R] [IsNilpotent L M] : traceForm R L M = 0 :=
  by
  ext x y
  simp only [traceForm_apply_apply, LinearMap.zero_apply, ← isNilpotent_iff_eq_zero]
  apply LinearMap.isNilpotent_trace_of_isNilpotent
  exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y

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