Theorem Matrix.PosSemidef.posDef_iff_mulVec_injective

Modification history

2026-09-15 23:40
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): generalize and golf `PosSemidef.posDef_iff_isUnit` (#43627)
Added Matrix.PosSemidef.posDef_iff_mulVec_injectiveView on Github →