posSemidef_self_mul_conjTranspose

English

Similarly, the matrix A Aᴴ is positive semidefinite.

Русский

Аналогично, матрица AAᴴ положительная полуопределенная.

LaTeX

$$$A A^H \succeq 0$$$

Lean4

/-- A matrix multiplied by its conjugate transpose is positive semidefinite -/
theorem posSemidef_self_mul_conjTranspose [StarOrderedRing R] (A : Matrix m n R) : PosSemidef (A * Aᴴ) := by
  simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ

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