feat: two lemmas about division (#9966)

Mathlib/Algebra/Group/Basic.lean

@@ -410,7 +410,7 @@ end DivInvOneMonoid
 
 section DivisionMonoid
 
-variable [DivisionMonoid α] {a b c : α}
+variable [DivisionMonoid α] {a b c d : α}
 
 attribute [local simp] mul_assoc div_eq_mul_inv
 
@@ -471,6 +471,10 @@ theorem one_div_one_div : 1 / (1 / a) = a := by simp
 #align one_div_one_div one_div_one_div
 #align zero_sub_zero_sub zero_sub_zero_sub
 
+@[to_additive]
+theorem div_eq_div_iff_comm : a / b = c / d ↔ b / a = d / c :=
+  inv_inj.symm.trans <| by simp only [inv_div]
+
 @[to_additive SubtractionMonoid.toSubNegZeroMonoid]
 instance (priority := 100) DivisionMonoid.toDivInvOneMonoid : DivInvOneMonoid α :=
   { DivisionMonoid.toDivInvMonoid with

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -150,6 +150,7 @@ theorem divp_mk0 (a : G₀) {b : G₀} (hb : b ≠ 0) : a /ₚ Units.mk0 b hb =
 
 namespace Commute
 
+/-- The `MonoidWithZero` version of `div_eq_div_iff_mul_eq_mul`. -/
 protected lemma div_eq_div_iff (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
     a / b = c / d ↔ a * d = c * b := hbd.div_eq_div_iff_of_isUnit hb.isUnit hd.isUnit
 
@@ -195,6 +196,12 @@ theorem div_eq_div_iff (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d =
   IsUnit.div_eq_div_iff hb.isUnit hd.isUnit
 #align div_eq_div_iff div_eq_div_iff
 
+/-- The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`. -/
+theorem div_eq_div_iff_div_eq_div' (hb : b ≠ 0) (hc : c ≠ 0) : a / b = c / d ↔ a / c = b / d := by
+  conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel _ hb]
+  conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel _ hc]
+  rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]
+
 theorem div_div_cancel' (ha : a ≠ 0) : a / (a / b) = b :=
   IsUnit.div_div_cancel ha.isUnit
 #align div_div_cancel' div_div_cancel'