mathlib3

8d13a2db - feat(algebra/order/rearrangement): Equality case of the Rearrangement Inequality (#13245)

feat(algebra/order/rearrangement): Equality case of the Rearrangement Inequality (#13245) This PR deduces the cases of equality and strict inequality of the Rearrangement Inequality as a corollary to the existing statement of the rearrangement inequality. Co-authored-by: YaelDillies <yael.dillies@gmail.com>