Commit 2026-09-15 23:40 224c3399

View on Github →

chore(LinearAlgebra/Matrix/PosDef): generalize and golf PosSemidef.posDef_iff_isUnit (#43627)

Estimated changes

Modified Mathlib/Analysis/Matrix/Order.lean

deleted theorem Matrix.PosSemidef.posDef_iff_det_ne_zero

deleted theorem Matrix.PosSemidef.posDef_iff_isUnit

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosDef.isUnit

added theorem Matrix.PosDef.mulVec_injective

added theorem Matrix.PosSemidef.posDef_iff_det_ne_zero

added theorem Matrix.PosSemidef.posDef_iff_isUnit

added theorem Matrix.PosSemidef.posDef_iff_mulVec_injective

added theorem Matrix.posDef_iff_posSemidef_and_mulVec_injective