Mathlib v3 is deprecated. Go to Mathlib v4

Theorem antivary.card_smul_sum_le_sum_smul_sum

Modification history

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