diff --git a/Mathlib/Analysis/Normed/Lp/WithLp.lean b/Mathlib/Analysis/Normed/Lp/WithLp.lean
index a3ec2990e2e8b..2a19919172b59 100644
--- a/Mathlib/Analysis/Normed/Lp/WithLp.lean
+++ b/Mathlib/Analysis/Normed/Lp/WithLp.lean
@@ -56,6 +56,7 @@ protected def equiv : WithLp p V ≃ V := Equiv.refl _
 
 instance instNontrivial [Nontrivial V] : Nontrivial (WithLp p V) := ‹Nontrivial V›
 instance instUnique [Unique V] : Unique (WithLp p V) := ‹Unique V›
+instance instDecidableEq [DecidableEq V] : DecidableEq (WithLp p V) := ‹DecidableEq V›
 
 variable [Semiring K] [Semiring K'] [AddCommGroup V]