diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f3a78bb221..c04cb9f729 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -357,4 +357,12 @@ def dropLast {α} : List α → List α
     simp[dropLast, ih]
     rfl
 
+def maximum? [LT α] [DecidableRel (@LT.lt α _)] : List α → Option α
+  | []    => none
+  | a::as => some <| as.foldl max a
+
+def minimum? [LE α] [DecidableRel (@LE.le α _)] : List α → Option α
+  | []    => none
+  | a::as => some <| as.foldl min a
+
 end List
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index d0e20b4561..df7de2544d 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -360,6 +360,12 @@ class LT (α : Type u) where lt : α → α → Prop
 @[reducible] def GE.ge {α : Type u} [LE α] (a b : α) : Prop := LE.le b a
 @[reducible] def GT.gt {α : Type u} [LT α] (a b : α) : Prop := LT.lt b a
 
+@[inline] def max [LT α] [DecidableRel (@LT.lt α _)] (a b : α) : α :=
+  ite (LT.lt b a) a b
+
+@[inline] def min [LE α] [DecidableRel (@LE.le α _)] (a b : α) : α :=
+  ite (LE.le a b) a b
+
 class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hAdd : α → β → γ