Commit 2025-04-17 11:01 6fb295ce

View on Github →

feat: x.swap < (b, a) ↔ x < (a, b) (#24124)

Estimated changes

modified theorem Prod.le_def
modified theorem Prod.mk_le_mk
added theorem Prod.mk_le_swap
added theorem Prod.mk_lt_swap
added theorem Prod.swap_le_mk
modified theorem Prod.swap_le_swap
added theorem Prod.swap_lt_mk