trace_mul_single — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem trace_mul_single [NonUnitalNonAssocSemiring R] [Fintype m] (x : Matrix m n R) (i : n) (j : m) (a : R) :
    (x * single i j a).trace = MulOpposite.op a • x j i := by simp [trace, mul_apply, single, ite_and]

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