chore(algebra/group/units): mark some lemmas as simp (#14871)

These seem like fairly natural candidates for simp lemmas.
leanprover-community · Jun 27, 2022 · cf50ac1 · cf50ac1
1 parent cad1a6c
commit cf50ac1
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
@@ -398,16 +398,16 @@ noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : Mˣ :=
 lemma is_unit.unit_of_coe_units [monoid M] {a : Mˣ} (h : is_unit (a : M)) : h.unit = a :=
 units.ext $ rfl
 
-@[to_additive]
+@[simp, to_additive]
 lemma is_unit.unit_spec [monoid M] {a : M} (h : is_unit a) : ↑h.unit = a :=
 rfl
 
-@[to_additive]
+@[simp, to_additive]
 lemma is_unit.coe_inv_mul [monoid M] {a : M} (h : is_unit a) :
   ↑(h.unit)⁻¹ * a = 1 :=
 units.mul_inv _
 
-@[to_additive]
+@[simp, to_additive]
 lemma is_unit.mul_coe_inv [monoid M] {a : M} (h : is_unit a) :
   a * ↑(h.unit)⁻¹ = 1 :=
 begin