English
For an invertible matrix M and any N, tr(M^{-1} N M) = tr(N).
Русский
Для обратимой M и любой N выполняется tr(M^{-1} N M) = tr(N).
LaTeX
$$$$ \\operatorname{trace}(M^{-1} N M) = \\operatorname{trace}(N). $$$$
Lean4
/-- Matrices `A` and `B` are equal iff `(A * x).trace = (B * x).trace` for all `x`. -/
theorem ext_iff_trace_mul_right [NonAssocSemiring R] {A B : Matrix m n R} :
A = B ↔ ∀ x, (A * x).trace = (B * x).trace :=
by
refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
ext i j
classical simpa [trace_mul_single] using h (single j i (1 : R))