ext_iff_trace_mul_right — Mathlib

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))

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