Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-25 12:01 b877056e

View on Github →

feat(order/compare): general cleanup (#15665) We add swap_inj, golf some lemmas, do some simple spacing tweaks.

Estimated changes

modified theorem cmp_swap
modified theorem ordering.compares.eq_eq
modified theorem ordering.compares.eq_lt
modified theorem ordering.compares.inj
modified theorem ordering.compares.le_total
modified theorem ordering.compares.ne_lt
added theorem ordering.swap_inj