posDef_conjTranspose_iff — Mathlib

English

A matrix is positive definite if and only if its conjugate transpose is positive definite.

Русский

Матрица положительно определена тогда и только тогда, когда её сопряжённо-транспонированная также положительно определена.

LaTeX

$$$$ \\operatorname{PosDef}(M^{\\mathrm{H}}) \\iff \\operatorname{PosDef}(M). $$$$

Lean4

@[simp]
theorem _root_.Matrix.posDef_conjTranspose_iff {M : Matrix n n R} : Mᴴ.PosDef ↔ M.PosDef :=
  ⟨(by simpa using ·.conjTranspose), .conjTranspose⟩

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