inv — Mathlib

English

A positive definite matrix is a unit (invertible) in the matrix ring.

Русский

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

LaTeX

$$$$ \\operatorname{PosDef}(M) \\Rightarrow \\operatorname{IsUnit} M. $$$$

Lean4

protected theorem inv [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) : M⁻¹.PosDef :=
  by
  have := hM.mul_mul_conjTranspose_same (B := M⁻¹) ?_
  · let _ := hM.isUnit.invertible
    simpa using this.conjTranspose
  · simp only [Matrix.vecMul_injective_iff_isUnit, isUnit_nonsing_inv_iff, hM.isUnit]

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