trace_conjTranspose_mul_self_eq_zero_iff

Mathlib.LinearAlgebra.Matrix.PosDef

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

← MathLib Explorer

English

(AᴴA).trace = 0 iff A = 0

Русский

(AᴴA).trace = 0 если и только если A = 0

LaTeX

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

Lean4

theorem trace_conjTranspose_mul_self_eq_zero_iff {A : Matrix m n R} : (Aᴴ * A).trace = 0 ↔ A = 0 := by
  rw [← star_vec_dotProduct_vec, dotProduct_star_self_eq_zero, vec_eq_zero_iff]

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

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

Разделы

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

Аффилиация

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