Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sq_sum_le_card_mul_sum_sq

Modification history

2023-02-02 08:56
src/algebra/order/chebyshev.lean
feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187) …
Added sq_sum_le_card_mul_sum_sqView on Github →