Commit 2026-09-01 23:21 07ecc8b1

View on Github →

feat: the L matrix in the LDL decomposition is lower triangular (#43290) The title. This closes an existing TODO in the file. I also updated one of the lemmas to use the predicate IsLowerTriangularinstead of spelling out the definition.

Estimated changes

Modified Mathlib/Analysis/Matrix/LDL.lean

added theorem LDL.isLowerTriangular_lower

added theorem LDL.isLowerTriangular_lowerInv

deleted theorem LDL.lowerInv_triangular