posDef_inv_iff — Mathlib

English

The inverse of a matrix preserves positive definiteness: M⁻¹ is PD if and only if M is PD.

Русский

Обратная матрица сохраняет положительную определенность: M⁻¹ положительно определена тогда и только тогда, когда M положительно определена.

LaTeX

$$$$ \\operatorname{PosDef}(M^{-1}) \\iff \\operatorname{PosDef}(M). $$$$

Lean4

@[simp]
theorem _root_.Matrix.posDef_inv_iff [DecidableEq n] {M : Matrix n n K} : M⁻¹.PosDef ↔ M.PosDef :=
  ⟨fun h =>
    letI := (Matrix.isUnit_nonsing_inv_iff.1 <| h.isUnit).invertible
    Matrix.inv_inv_of_invertible M ▸ h.inv,
    (·.inv)⟩

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