Commit 2023-12-04 20:02 21b63753

View on Github →

refactor(LinearAlgebra/Matrix/PosDef): separate PosDef lemmas from PosSemidef lemmas (#8810) There are no new or deleted lemmas here, only a reordering; but to enable dot notation I have renamed:

  • posDef_toQuadraticForm' to PosDef.toQuadraticForm'
  • posDef_of_toQuadraticForm' to PosDef.of_toQuadraticForm' Split from #8809

Estimated changes

modified theorem Matrix.PosDef.det_pos
modified theorem Matrix.PosDef.isHermitian
modified theorem Matrix.PosDef.posSemidef
modified theorem Matrix.PosDef.transpose