feat: add DecidableEq instances for Multiplicative and Additive (…

…#8072)
leanprover-community · Nov 1, 2023 · 056e725 · 056e725
1 parent f294621
commit 056e725
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean
@@ -132,6 +132,10 @@ instance [h: Infinite α] : Infinite (Additive α) := h
 
 instance [h: Infinite α] : Infinite (Multiplicative α) := h
 
+instance [h : DecidableEq α] : DecidableEq (Multiplicative α) := h
+
+instance [h : DecidableEq α] : DecidableEq (Additive α) := h
+
 instance instNontrivialAdditive [Nontrivial α] : Nontrivial (Additive α) :=
   ofMul.injective.nontrivial
 #align additive.nontrivial instNontrivialAdditive