Commit 2023-06-15 17:27 cc3528b5

View on Github →

feat: port LinearAlgebra.Matrix.PosDef (#5060)

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/PosDef.lean

added def Matrix.InnerProductSpace.ofMatrix

added theorem Matrix.PosDef.det_pos

added theorem Matrix.PosDef.isHermitian

added theorem Matrix.PosDef.posSemidef

added theorem Matrix.PosDef.transpose

added def Matrix.PosDef

added theorem Matrix.PosSemidef.submatrix

added def Matrix.PosSemidef

added theorem Matrix.posDef_of_toQuadraticForm'

added theorem Matrix.posDef_toQuadraticForm'

added theorem Matrix.posSemidef_submatrix_equiv

added theorem QuadraticForm.posDef_of_toMatrix'

added theorem QuadraticForm.posDef_toMatrix'