Commit 2024-10-01 21:09 a95d25fa

View on Github →

feat: M⁻¹.PosDef ↔ M.PosDef (#17310) The implication already existed for PosSemidef

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.PosDef.isUnit

added theorem Matrix.posDef_inv_iff