Theorem Finset.sum_sq_le_sq_sum_of_nonneg

Modification history

2024-08-19 19:19
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
feat: constructions of Hilbert C⋆-modules (#15765) …
Added Finset.sum_sq_le_sq_sum_of_nonnegView on Github →