Commit 2025-10-08 02:34 e503dc1c

View on Github →

chore(LinearAlgebra/Matrix/PosDef): deprecate PosSemidef.sqrt in favour of CFC (#29896) We deprecate PosSemidef.sqrt and all related results in favour of using more general results (i.e., CFC.sqrt and results in C*-algebras). This also defines the partial order and StarOrderedRing instances on matrices. This also moves all results related to PosSemidef.sqrt to Analysis/Matrix/Order to minimize imports. The partial order instance on matrices is scoped to MatrixOrder (analogous to ComplexOrder).

Estimated changes

added theorem commute_iff_mul_nonneg
added theorem Matrix.le_iff
added theorem CFC.sq_eq_sq_iff
added theorem CFC.sqrt_eq_one_iff'
added theorem CFC.sqrt_eq_one_iff
deleted theorem Matrix.PosDef.commute_iff
deleted theorem Matrix.PosDef.posDef_sqrt
deleted theorem Matrix.PosSemidef.sq_sqrt
deleted theorem Matrix.PosSemidef.sqrt_sq