From 056e7257480ba893727fd5804ff236ef24a8ea63 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 1 Nov 2023 00:15:40 +0000 Subject: [PATCH] feat: add `DecidableEq` instances for `Multiplicative` and `Additive` (#8072) --- Mathlib/Algebra/Group/TypeTags.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean index cf5ed1aa6b851..a0a6bd6797e2f 100644 --- 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