Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monovary_on.sum_mul_sum_le_card_mul_sum

Modification history

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