chore: WithLp inherits decidable equality (#22250)

leanprover-community · Feb 24, 2025 · 4ea41dd · 4ea41dd
1 parent 69f2481
commit 4ea41dd
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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]