Theorem Matrix.PosSemidef.posDef_iff_det_ne_zero

Modification history

2026-09-15 23:40
Mathlib/Analysis/Matrix/Order.lean
chore(LinearAlgebra/Matrix/PosDef): generalize and golf `PosSemidef.posDef_iff_isUnit` (#43627)
Modified Matrix.PosSemidef.posDef_iff_det_ne_zeroView on Github →
2026-04-14 17:36
Mathlib/Analysis/Matrix/Order.lean
feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent (#37918) …
Added Matrix.PosSemidef.posDef_iff_det_ne_zeroView on Github →