Theorem Matrix.posDef_iff_eq_conjTranspose_mul_self

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

2025-08-07 15:06

Mathlib/LinearAlgebra/Matrix/PosDef.lean

chore(LinearAlgebra/Matrix/PosDef): lemma in wrong namespace (#28084) …

Added Matrix.posDef_iff_eq_conjTranspose_mul_self View on Github →