matrix_trace_commutator_zero — Mathlib

English

For any matrices X,Y over a field or ring, the trace of their commutator is zero: tr([X,Y]) = 0.

Русский

Для любых матриц X,Y над кольцом/полем след их коммутатора равен нулю: Tr([X,Y]) = 0.

LaTeX

$$$$ \operatorname{trace}([X,Y]) = 0. $$$$

Lean4

@[simp]
theorem matrix_trace_commutator_zero [Fintype n] (X Y : Matrix n n R) : Matrix.trace ⁅X, Y⁆ = 0 :=
  calc
    _ = Matrix.trace (X * Y) - Matrix.trace (Y * X) := trace_sub _ _
    _ = Matrix.trace (X * Y) - Matrix.trace (X * Y) := (congr_arg (fun x => _ - x) (Matrix.trace_mul_comm Y X))
    _ = 0 := sub_self _

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