Theorem Matrix.PosDef.isUnit

Modification history

2026-09-15 23:40
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): generalize and golf `PosSemidef.posDef_iff_isUnit` (#43627)
Modified Matrix.PosDef.isUnitView on Github →
2025-08-19 08:35
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): slight generalization for `PosDef.isUnit` (#28463) …
Modified Matrix.PosDef.isUnitView on Github →
2024-10-01 21:09
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: `M⁻¹.PosDef ↔ M.PosDef` (#17310) …
Added Matrix.PosDef.isUnitView on Github →