ext_iff_trace_mul_left — Mathlib

English

Matrices A and B are equal iff for all x, tr(Ax) = tr(Bx).

Русский

Матрицы A и B равны тогда и только тогда, когда для всех x выполняется tr(Ax) = tr(Bx).

LaTeX

$$$$ A = B \\iff \\forall x, \\operatorname{trace}(A x) = \\operatorname{trace}(B x). $$$$

Lean4

/-- Matrices `A` and `B` are equal iff `(x * A).trace = (x * B).trace` for all `x`. -/
theorem ext_iff_trace_mul_left [NonAssocSemiring R] {A B : Matrix m n R} : A = B ↔ ∀ x, (x * A).trace = (x * B).trace :=
  by
  refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
  ext i j
  classical simpa [trace_single_mul] using h (single j i (1 : R))

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