isUnit — Mathlib

English

A positive definite matrix remains positive definite after taking the inverse.

Русский

Положительно определенная матрица остается положительно определенной после взятия обратной.

LaTeX

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

Lean4

theorem isUnit [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) : IsUnit M :=
  by
  by_contra h
  obtain ⟨a, ha, ha2⟩ : ∃ a ≠ 0, M *ᵥ a = 0 :=
    by
    obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩
  simpa [ha2] using hM.2 _ ha

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