Commit 2024-09-19 11:58 3f70ca89

View on Github →

chore: generalise the binary rearrangement inequality (#16940)

Estimated changes

Modified Mathlib/Algebra/Order/Module/Defs.lean

modified theorem smul_add_smul_le_smul_add_smul'

modified theorem smul_add_smul_le_smul_add_smul

modified theorem smul_add_smul_lt_smul_add_smul'

modified theorem smul_add_smul_lt_smul_add_smul