Theorems · Definition · linear algebra

LDL.lowerInv

{𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [WellFoundedLT n] → [LocallyFiniteOrderBot n] → {S : Matrix n n 𝕜} → [Fintype n] → S.PosDef → Matrix n n 𝕜

The inverse of the lower triangular matrix L of the LDL-decomposition. It is obtained by applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by Sᵀ on the standard basis vectors Pi.basisFun.

Defined in

Mathlib.Analysis.Matrix.LDL

Cited by

6 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeLinearOrderWellFoundedLTLocallyFiniteOrderBotFintype