trace_mul_conjTranspose_self_eq_zero_iff

Mathlib.LinearAlgebra.Matrix.PosDef

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

← MathLib Explorer

English

Same statement for A Aᴴ: trace equals zero iff A = 0.

Русский

Аналогично для AAᴴ: trace ноль тогда и только тогда, когда A = 0.

LaTeX

$$$(A A^H).\operatorname{trace} = 0 \iff A = 0$$$

Lean4

theorem trace_mul_conjTranspose_self_eq_zero_iff {A : Matrix m n R} : (A * Aᴴ).trace = 0 ↔ A = 0 := by
  simpa using trace_conjTranspose_mul_self_eq_zero_iff (A := Aᴴ)

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

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

Разделы

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

Аффилиация

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