Mathlib v3 is deprecated. Go to Mathlib v4

Theorem antivary_on.card_mul_sum_le_sum_mul_sum

Modification history

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