Theorem Matrix.PosSemidef.sqrt_sq

Modification history

2025-10-08 02:34

Mathlib/Analysis/Matrix/Order.lean

chore(LinearAlgebra/Matrix/PosDef): deprecate `PosSemidef.sqrt` in favour of `CFC` (#29896) …

Modified Matrix.PosSemidef.sqrt_sq View on Github →

2023-12-18 20:33

Mathlib/LinearAlgebra/Matrix/PosDef.lean

feat(LinearAlgebra/Matrix/PosDef): unique positive semidef square root (#8809) …

Added Matrix.PosSemidef.sqrt_sq View on Github →