Theorem Matrix.PosSemidef.trace_eq_zero_iff

Modification history

2025-10-08 02:34

Mathlib/LinearAlgebra/Matrix/PosDef.lean

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

Added Matrix.PosSemidef.trace_eq_zero_iff View on Github →