mathlib
2aa08c1f - chore(algebra/ordered_group): merge `add_le_add'` with `add_le_add` (#3159)

Commit

5 years ago

chore(algebra/ordered_group): merge `add_le_add'` with `add_le_add` (#3159) Also drop `mul_le_mul''` (was a weaker version of `mul_le_mul'`).

Author

urkud

Parents