chore: Ord instance for Prod.Lex (#6090)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 31, 2023 · c8f191d · c8f191d
1 parent 795a5ff
commit c8f191d
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean
@@ -150,6 +150,9 @@ instance linearOrder (α β : Type _) [LinearOrder α] [LinearOrder β] : Linear
     decidableEq := Lex.decidableEq _ _, }
 #align prod.lex.linear_order Prod.Lex.linearOrder
 
+instance [Ord α] [Ord β] : Ord (α ×ₗ β) where
+  compare := compareLex (compareOn (·.1)) (compareOn (·.2))
+
 instance orderBot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] : OrderBot (α ×ₗ β) where
   bot := toLex ⊥
   bot_le _ := toLex_mono bot_le