Theorem Matrix.PosDef.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.PosDef.mulVec_injective View on Github →