Documentation Verification Report

LDL

📁 Source: Mathlib/Analysis/Matrix/LDL.lean

Statistics

Metric	Count
Definitions `diag`, `diagEntries`, `invertibleLowerInv`, `lower`, `lowerInv`	5
Theorems `diag_eq_lowerInv_conj`, `lowerInv_eq_gramSchmidtBasis`, `lowerInv_orthogonal`, `lowerInv_triangular`, `lower_conj_diag`	5
Total	10

LDL

Definitions

Name	Category	Theorems
`diag` 📖	CompOp	2 math math: `lower_conj_diag`, `diag_eq_lowerInv_conj`
`diagEntries` 📖	CompOp	—
`invertibleLowerInv` 📖	CompOp	—
`lower` 📖	CompOp	1 math math: `lower_conj_diag`
`lowerInv` 📖	CompOp	4 math math: `lowerInv_eq_gramSchmidtBasis`, `lowerInv_orthogonal`, `lowerInv_triangular`, `diag_eq_lowerInv_conj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diag_eq_lowerInv_conj` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`diag` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `lowerInv` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`Matrix.ext` `Matrix.diagonal.congr_simp` `Matrix.diagonal_apply_eq` `star_star` `dotProduct_comm` `Matrix.mul_assoc` `Matrix.diagonal_apply_ne` `Matrix.mul_mul_apply` `Matrix.conjTranspose.eq_1` `Matrix.transpose_map` `Matrix.transpose_transpose` `Matrix.dotProduct_mulVec` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `lowerInv_orthogonal` `inner_conj_symm` `Matrix.mulVec_transpose` `EuclideanSpace.inner_toLp_toLp` `RCLike.star_def` `Matrix.star_dotProduct_star`
`lowerInv_eq_gramSchmidtBasis` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`lowerInv` `Matrix.transpose` `Module.Basis.toMatrix` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Pi.Function.module` `Semiring.toModule` `Pi.basisFun` `Finite.of_fintype` `DFunLike.coe` `Module.Basis` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Matrix.toNormedAddCommGroup` `Matrix.PosDef.transpose` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Matrix.toInnerProductSpace` `Matrix.PosDef.posSemidef` `CommRing.toRing` `Module.Basis.instFunLike` `InnerProductSpace.gramSchmidtBasis`	—	`Matrix.ext` `Finite.of_fintype` `Matrix.PosDef.transpose` `Matrix.PosDef.posSemidef` `lowerInv.eq_1` `Module.Basis.coePiBasisFun.toMatrix_eq_transpose` `InnerProductSpace.coe_gramSchmidtBasis`
`lowerInv_orthogonal` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Inner.inner` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `WithLp.toLp` `lowerInv` `Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Matrix.transpose` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`InnerProductSpace.gramSchmidt_orthogonal` `Matrix.PosDef.transpose` `Matrix.PosDef.posSemidef` `Finite.of_fintype`
`lowerInv_triangular` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`lowerInv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`RingHomInvPair.ids` `Matrix.PosDef.transpose` `Matrix.PosDef.posSemidef` `Finite.of_fintype` `InnerProductSpace.gramSchmidt_triangular` `Pi.basisFun_repr` `lowerInv.eq_1`
`lower_conj_diag` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `lower` `diag` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`lower.eq_1` `Matrix.conjTranspose_nonsing_inv` `Matrix.mul_assoc` `Matrix.inv_mul_eq_iff_eq_mul_of_invertible` `Matrix.mul_inv_eq_iff_eq_mul_of_invertible` `diag_eq_lowerInv_conj`

---

← Back to Index