trace_conj' — Mathlib

English

Let M be an invertible square matrix over a commutative ring α and N any square matrix of the same size. Then the trace is invariant under conjugation by M: tr(M^{-1} N M) = tr(N).

Русский

Пусть M — обратимая квадратная матрица над коммутативным кольцом α, а N — любая квадратная матрица того же размера. Тогда след остается неизменным при подобии: tr(M^{-1} N M) = tr(N).

LaTeX

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

Lean4

/-- A variant of `Matrix.trace_units_conj'`. -/
theorem trace_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : trace (M⁻¹ * N * M) = trace N := by
  rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']

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