Commit 2024-12-07 13:24 4fb35bfa

View on Github →

feat(Order/Basic): PartialOrder.ext_lt (#19724) Two partial / linear orders with the same < relation are the same.

Estimated changes

added theorem LinearOrder.ext_lt
added theorem PartialOrder.ext_lt