Commit 2023-06-16 02:09 b4efa00f

View on Github →

feat: port LinearAlgebra.Matrix.LDL (#5061)

depends on: #4920
depends on: #5058
depends on: #5059
depends on: #5060

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/LDL.lean

added theorem LDL.diag_eq_lowerInv_conj

added theorem LDL.lowerInv_eq_gramSchmidtBasis

added theorem LDL.lowerInv_orthogonal

added theorem LDL.lowerInv_triangular

added theorem LDL.lower_conj_diag

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean