diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index 3dc905ce7430d..787a5948b5f09 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -111,6 +111,8 @@ section monoid
   theorem divp_assoc (a b : α) (u : units α) : a * b /ₚ u = a * (b /ₚ u) :=
   mul_assoc _ _ _
 
+  @[simp] theorem divp_inv (x : α) (u : units α) : a /ₚ u⁻¹ = a * u := rfl
+
   @[simp] theorem divp_mul_cancel (a : α) (u : units α) : a /ₚ u * u = a :=
   (mul_assoc _ _ _).trans $ by rw [units.inv_mul, mul_one]
 
@@ -120,7 +122,13 @@ section monoid
   @[simp] theorem divp_right_inj (u : units α) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b :=
   units.mul_right_inj _
 
-  theorem divp_eq_one (a : α) (u : units α) : a /ₚ u = 1 ↔ a = u :=
+  theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : units α) : (x /ₚ u₁) /ₚ u₂ = x /ₚ (u₂ * u₁) :=
+  by simp only [divp, mul_inv_rev, units.coe_mul, mul_assoc]
+
+  theorem divp_eq_iff_mul_eq (x : α) (u : units α) (y : α) : x /ₚ u = y ↔ y * u = x :=
+  u.mul_right_inj.symm.trans $ by rw [divp_mul_cancel]; exact ⟨eq.symm, eq.symm⟩
+
+  theorem divp_eq_one_iff_eq (a : α) (u : units α) : a /ₚ u = 1 ↔ a = u :=
   (units.mul_right_inj u).symm.trans $ by rw [divp_mul_cancel, one_mul]
 
   @[simp] theorem one_divp (u : units α) : 1 /ₚ u = ↑u⁻¹ :=
@@ -128,6 +136,20 @@ section monoid
 
 end monoid
 
+section comm_monoid
+
+variables [comm_monoid α]
+
+theorem divp_eq_divp_iff {x y : α} {ux uy : units α} :
+  x /ₚ ux = y /ₚ uy ↔ x * uy = y * ux :=
+by rw [divp_eq_iff_mul_eq, mul_comm, ← divp_assoc, divp_eq_iff_mul_eq, mul_comm y ux]
+
+theorem divp_mul_divp (x y : α) (ux uy : units α) :
+  (x /ₚ ux) * (y /ₚ uy) = (x * y) /ₚ (ux * uy) :=
+by rw [← divp_divp_eq_divp_mul, divp_assoc, mul_comm x, divp_assoc, mul_comm]
+
+end comm_monoid
+
 section group
   variables [group α]