Commit 2026-09-09 15:18 2cc1b885
View on Github →chore(LinearAlgebra/Matrix/PosDef): generalize PosSemidef.dotProduct_mulVec_zero_iff (#43617)
Found from reviewing #43460.
Also decrease imports in Combinatorics/SimpleGraph/LapMatrix by ~25%.
Initial long and tedious proof of the generalization is by Claude (hence the label), golfed by me.