diff --git a/Std/Data/BinomialHeap/Basic.lean b/Std/Data/BinomialHeap/Basic.lean
index c3051ad42e..e21a79d9bc 100644
--- a/Std/Data/BinomialHeap/Basic.lean
+++ b/Std/Data/BinomialHeap/Basic.lean
@@ -502,6 +502,7 @@ variable {α : Type u} {le : α → α → Bool}
 /-- `O(1)`. Make a new empty binomial heap. -/
 @[inline] def empty : BinomialHeap α le := mkBinomialHeap α le
 
+instance : EmptyCollection (BinomialHeap α le) := ⟨.empty⟩
 instance : Inhabited (BinomialHeap α le) := ⟨.empty⟩
 
 /-- `O(1)`. Is the heap empty? -/