feat(algebra/group_with_zero/units): add ring.inverse lemmas (#16889)

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 :=