trace_conj — Mathlib

English

Trace is invariant under conjugation by a unit: trace(M N M^{-1}) = trace N.

Русский

След матрицы неизменен при сопряжении единицей: trace(M N M^{-1}) = trace N.

LaTeX

$$trace (M * N * M⁻¹) = trace 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]

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