trace_single_eq_same

Mathlib.LinearAlgebra.Matrix.Trace

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

English

For the diagonal entry, trace equals the value c on the diagonal: tr(single(i,i,c)) = c.

Русский

Для диагонального элемента: tr(single(i,i,c)) = c.

LaTeX

$$$$ \\operatorname{trace}(\\mathrm{single}(i,i,c)) = c. $$$$

Lean4

@[simp]
theorem trace_single_eq_same : trace (single i i c) = c := by simp [trace]

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

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

Разделы

Аффилиация

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