inv — Mathlib

English

If M is PSD and invertible, then M^{-1} is PSD.

Русский

Если M ПСД и обратима, то M^{-1} ПСД.

LaTeX

$$$\text{PosSemidef}(M) \land \det M \neq 0 \Rightarrow \text{PosSemidef}(M^{-1})$$$

Lean4

protected theorem inv [DecidableEq n] {M : Matrix n n R'} (hM : M.PosSemidef) : M⁻¹.PosSemidef :=
  by
  by_cases h : IsUnit M.det
  · have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose
    rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this
  · rw [nonsing_inv_apply_not_isUnit _ h]
    exact .zero

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