Theorem Finsupp.sum_pos

Modification history

2025-12-09 04:22

Mathlib/Data/Finsupp/Order.lean

refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)

Added Finsupp.sum_pos View on Github →