Theorem Matrix.posDef_inv_iff

Modification history

2025-08-19 08:35
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): slight generalization for `PosDef.isUnit` (#28463) …
Modified Matrix.posDef_inv_iffView on Github →
2024-10-01 21:09
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: `M⁻¹.PosDef ↔ M.PosDef` (#17310) …
Added Matrix.posDef_inv_iffView on Github →