Theorems · Theorem · linear algebra
LDL.lowerInv_eq_gramSchmidtBasis
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
[inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
LDL.lowerInv hS = ((Pi.basisFun 𝕜 n).toMatrix ⇑(InnerProductSpace.gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose- Defined in
- Mathlib.Analysis.Matrix.LDL
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- NormedAddCommGroupproof · cited by 15,752
- LinearOrderstatement and proof · cited by 8,572
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- InnerProductSpaceproof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- Module.Basisstatement · cited by 1,477
- Matrix.extproof · cited by 540
- WellFoundedLTstatement and proof · cited by 491
- Matrix.transposestatement and proof · cited by 389
- LocallyFiniteOrderBotstatement and proof · cited by 286
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.