mathlib

aebd3428 - feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187)

feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187) Prove Chebyshev's sum inequality as a corollary to the rearrangement inequality. Co-authored-by: YaelDillies <yael.dillies@gmail.com> Co-authored-by: Mantas Bakšys <39908973+MantasBaksys@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>