trace_fin_one

Mathlib.LinearAlgebra.Matrix.Trace

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

English

If A is a 1×1 matrix with entry a, then tr(A) = a.

Русский

Если A — матрица 1×1 со значением a, то tr(A) = a.

LaTeX

$$$$ \\operatorname{trace}(A) = A_{0,0}. $$$$

Lean4

theorem trace_fin_one (A : Matrix (Fin 1) (Fin 1) R) : trace A = A 0 0 :=
  add_zero _

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

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

Разделы

Аффилиация

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