trace_units_conj — Mathlib

English

For an invertible matrix M, and any N of the same size, tr(M N M^{-1}) = tr(N).

Русский

Для обратимой матрицы M и любой матрицы N одинакового размера след сохраняется under сопряжение: tr(M N M^{-1}) = tr(N).

LaTeX

$$$$ \\operatorname{trace}(M N M^{-1}) = \\operatorname{trace}(N). $$$$

Lean4

theorem trace_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace ((M : Matrix _ _ _) * N * (↑M⁻¹ : Matrix _ _ _)) = trace N := by rw [trace_mul_cycle, Units.inv_mul, one_mul]

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