Commit 2023-08-16 16:11 ee8a9190

View on Github →

refactor(LinearAlgebra/Matrix/PosDef): Generalize to StarOrderedRing (#6489) I assume this is mathematically sound, though right now we can't generalize many dependencies due to the reliance of InnerProductSpace.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosDef.isHermitian

modified theorem Matrix.PosDef.posSemidef

added theorem Matrix.PosDef.re_dotProduct_pos

modified theorem Matrix.PosDef.transpose

modified def Matrix.PosDef

added theorem Matrix.PosSemidef.re_dotProduct_nonneg

modified theorem Matrix.PosSemidef.submatrix

modified def Matrix.PosSemidef

modified theorem Matrix.posSemidef_conjTranspose_mul_self

modified theorem Matrix.posSemidef_self_mul_conjTranspose

modified theorem Matrix.posSemidef_submatrix_equiv

Modified Mathlib/LinearAlgebra/Matrix/SchurComplement.lean