diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index abdcea88f4911..f96bfe3abd2cc 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -415,6 +415,9 @@ begin
   simp [h.unit_spec]
 end
 
+/-- `is_unit x` is decidable if we can decide if `x` comes from `Mˣ`. -/
+instance [monoid M] (x : M) [h : decidable (∃ u : Mˣ, ↑u = x)] : decidable (is_unit x) := h
+
 section monoid
 variables [monoid M] {a b c : M}