Theorem Matrix.PosSemidef.eq_of_sq_eq_sq

Modification history

2025-10-08 02:34

Mathlib/LinearAlgebra/Matrix/PosDef.lean

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

Deleted Matrix.PosSemidef.eq_of_sq_eq_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.eq_of_sq_eq_sq View on Github →