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 →