Theorem Matrix.PosSemidef.sqrt_eq_one_iff

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_eq_one_iff View on Github →

2025-05-07 23:30

Mathlib/LinearAlgebra/Matrix/PosDef.lean

feat(Matrix/PosDef): decomposition into units (#24647) …

Added Matrix.PosSemidef.sqrt_eq_one_iff View on Github →