traceAux_def

Mathlib.LinearAlgebra.Trace

URI: https://scilib.ai/kg/mathlib#LinearMap.traceAux_def

English

For any f, traceAux R b f equals the matrix trace of toMatrix b b f.

Русский

Для любого f traceAux R b f равно следу матрицы toMatrix b b f.

LaTeX

$$$\\text{traceAux}_R(b)(f) = \\mathrm{tr}( \\mathrm{toMatrix}_b^b f )$$$

Lean4

theorem traceAux_def (b : Basis ι R M) (f : M →ₗ[R] M) : traceAux R b f = Matrix.trace (LinearMap.toMatrix b b f) :=
  rfl

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

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

Разделы

Аффилиация

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