trace_eq_zero_of_isEmpty

Mathlib.LinearAlgebra.Matrix.Trace

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

English

If the index set is empty (IsEmpty n), then tr(A) = 0 for any matrix A.

Русский

Если индексное множество пустое, то tr(A) = 0 для любой матрицы A.

LaTeX

$$$$ [IsEmpty n] \Rightarrow \operatorname{tr}(A) = 0 $$$$

Lean4

@[simp]
theorem trace_eq_zero_of_isEmpty [IsEmpty n] (A : Matrix n n R) : trace A = 0 := by simp [trace]

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

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

Разделы

Аффилиация

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