diff --git a/src/algebra/group_with_zero/units.lean b/src/algebra/group_with_zero/units.lean
index 00589fb05a5f1..b075720ba2f9b 100644
--- a/src/algebra/group_with_zero/units.lean
+++ b/src/algebra/group_with_zero/units.lean
@@ -97,6 +97,15 @@ by rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
 lemma inverse_mul_cancel_left (x y : M₀) (h : is_unit x) : inverse x * (x * y) = y :=
 by rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
 
+lemma inverse_mul_eq_iff_eq_mul (x y z : M₀) (h : is_unit x) :
+  inverse x * y = z ↔ y = x * z :=
+⟨λ h1, by rw [← h1, mul_inverse_cancel_left _ _ h], λ h1, by rw [h1, inverse_mul_cancel_left _ _ h]⟩
+
+lemma eq_mul_inverse_iff_mul_eq (x y z : M₀) (h : is_unit z) :
+  x = y * inverse z ↔ x * z = y :=
+⟨λ h1, by rw [h1, inverse_mul_cancel_right _ _ h],
+  λ h1, by rw [← h1, mul_inverse_cancel_right _ _ h]⟩
+
 variables (M₀)
 
 @[simp] lemma inverse_one : inverse (1 : M₀) = 1 :=