trace_single_mul

Mathlib.LinearAlgebra.Matrix.Trace

URI: https://scilib.ai/kg/mathlib#Matrix.trace_single_mul

← MathLib Explorer

English

For any i, j and a, and any X, tr(single(i j a) X) = a · X_{j i}.

Русский

Для любого i, j, a и X: tr( single(i,j,a) X ) = a · X_{j i}.

LaTeX

$$$$ \\operatorname{trace}(\\mathrm{single}(i,j,a) \\cdot X) = a \\cdot X_{j i}. $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru