mathlib3

9becbc7c - feat(algebra/order/rearrangement) : Rearrangement Inequality (#10861)

feat(algebra/order/rearrangement) : Rearrangement Inequality (#10861) A range of variants of the rearrangement inequality. This is stated with scalar multiplication of a linear ring over an additive linear group, rather than having everything be in a linear ring. We couldn't find general statements of the rearrangement inequality in the literature, but this very much seems like an improvement. Co-authored-by: YaelDillies <yael.dillies@gmail.com> Co-authored-by: Mantas Bakšys <39908973+MantasBaksys@users.noreply.github.com>