chore(algebra/group/units): is_add_unit.decidable (#18439)

pechersky · pechersky · commit 369525b73f22 · 2023-02-14T16:30:16.000Z
Missing `to_additive` I had actually added this to mathlib4 3 months ago in leanprover-community/mathlib4@cbc0834 (leanprover-community/mathlib4#549), and never noticed it wasn't in mathlib3. mathlib4 hash-update placeholder pr: leanprover-community/mathlib4#2278
diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
@@ -458,6 +458,7 @@ lemma coe_inv_mul (h : is_unit a) : ↑(h.unit)⁻¹ * a = 1 := units.mul_inv _
 by convert h.unit.mul_inv
 
 /-- `is_unit x` is decidable if we can decide if `x` comes from `Mˣ`. -/
+@[to_additive "`is_add_unit x` is decidable if we can decide if `x` comes from `add_units M"]
 instance (x : M) [h : decidable (∃ u : Mˣ, ↑u = x)] : decidable (is_unit x) := h
 
 @[to_additive] lemma mul_left_inj (h : is_unit a) : b * a = c * a ↔ b = c :=
