chore(algebra/{group,group_with_zero}/basic): rename div_mul_div and div_mul_comm (#12365)

The new name, `div_mul_div_comm` is consistent with `mul_mul_mul_comm`.

Obviously this renames the additive versions too.

Author: eric-wieser

src/algebra/big_operators/multiset.lean

@@ -226,7 +226,7 @@ by { convert (m.map f).prod_hom (inv_monoid_with_zero_hom : α →*₀ α), rw m
 
 @[simp]
 lemma prod_map_div₀ : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
-m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div _ _ _ _).symm) (div_one _) _ _
+m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div_comm₀ _ _ _ _).symm) (div_one _) _ _
 
 lemma prod_map_zpow₀ {n : ℤ} : prod (m.map $ λ i, f i ^ n) = (m.map f).prod ^ n :=
 by { convert (m.map f).prod_hom (zpow_group_hom₀ _ : α →* α), rw map_map, refl }

src/algebra/group/basic.lean

@@ -480,7 +480,7 @@ lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c :=
 by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
 
 @[to_additive]
-lemma div_mul_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
+lemma div_mul_div_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_assoc,
   mul_left_cancel_iff, mul_comm, mul_assoc]
 

src/algebra/group/prod.lean

@@ -502,6 +502,6 @@ def div_monoid_with_zero_hom [comm_group_with_zero α] : α × α →*₀ α :=
 { to_fun := λ a, a.1 / a.2,
   map_zero' := zero_div _,
   map_one' := div_one _,
-  map_mul' := λ a b, (div_mul_div _ _ _ _).symm }
+  map_mul' := λ a b, (div_mul_div_comm₀ _ _ _ _).symm }
 
 end bundled_mul_div

src/algebra/group_with_zero/basic.lean

@@ -968,7 +968,7 @@ by rw [mul_comm, (div_mul_cancel _ hb)]
 
 local attribute [simp] mul_assoc mul_comm mul_left_comm
 
-lemma div_mul_div (a b c d : G₀) :
+lemma div_mul_div_comm₀ (a b c d : G₀) :
       (a / b) * (c / d) = (a * c) / (b * d) :=
 by simp [div_eq_mul_inv, mul_inv₀]
 
@@ -981,7 +981,7 @@ by simp [div_eq_mul_inv]
 
 lemma div_mul_eq_mul_div_comm (a b c : G₀) :
       (b / c) * a = b * (a / c) :=
-by rw [div_mul_eq_mul_div, ← one_mul c, ← div_mul_div, div_one, one_mul]
+by rw [div_mul_eq_mul_div, ← one_mul c, ← div_mul_div_comm₀, div_one, one_mul]
 
 lemma mul_eq_mul_of_div_eq_div (a : G₀) {b : G₀} (c : G₀) {d : G₀} (hb : b ≠ 0)
       (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b :=
@@ -990,7 +990,7 @@ by rw [← mul_one (a*d), mul_assoc, mul_comm d, ← mul_assoc, ← div_self hb,
 
 @[field_simps] lemma div_div_eq_div_mul (a b c : G₀) :
       (a / b) / c = a / (b * c) :=
-by rw [div_eq_mul_one_div, div_mul_div, mul_one]
+by rw [div_eq_mul_one_div, div_mul_div_comm₀, mul_one]
 
 lemma div_div_div_div_eq (a : G₀) {b c d : G₀} :
       (a / b) / (c / d) = (a * d) / (b * c) :=

src/algebra/order/lattice_group.lean

@@ -382,7 +382,7 @@ begin
     rw [sup_right_idem, sup_assoc, inf_assoc],
     nth_rewrite 3 inf_comm,
     rw [inf_right_idem, inf_assoc], }
-  ... = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) /(((b ⊓ a) ⊔ c) * (b ⊓ a ⊓ c)) : by rw div_mul_comm
+  ... = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) /(((b ⊓ a) ⊔ c) * (b ⊓ a ⊓ c)) : by rw div_mul_div_comm
   ... = (b ⊔ a) * c / ((b ⊓ a) * c) :
     by rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
   ... = (b ⊔ a) / (b ⊓ a) : by rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left,

src/analysis/box_integral/partition/additive.lean

@@ -176,7 +176,7 @@ of_map_split_add
     rw with_top.coe_le_coe at hJ,
     refine i.succ_above_cases _ _ j,
     { intros x hx,
-      simp only [box.split_lower_def hx, box.split_upper_def hx, update_same, 
+      simp only [box.split_lower_def hx, box.split_upper_def hx, update_same,
         ← with_bot.some_eq_coe, option.elim, box.face, (∘), update_noteq (fin.succ_above_ne _ _)],
       abel },
     { clear j, intros j x hx,
@@ -189,7 +189,7 @@ of_map_split_add
       simp only [box.split_lower_def hx, box.split_upper_def hx,
         box.split_lower_def hx', box.split_upper_def hx',
         ← with_bot.some_eq_coe, option.elim, box.face_mk,
-        update_noteq (fin.succ_above_ne _ _).symm, sub_add_comm,
+        update_noteq (fin.succ_above_ne _ _).symm, sub_add_sub_comm,
         update_comp_eq_of_injective _ i.succ_above.injective j x, ← hf],
       simp only [box.face] }
   end

src/analysis/mean_inequalities.lean

@@ -340,7 +340,7 @@ begin
   let f' := λ i, (f i) / (∑ i in s, (f i) ^ p) ^ (1 / p),
   let g' := λ i, (g i) / (∑ i in s, (g i) ^ q) ^ (1 / q),
   suffices : ∑ i in s, f' i * g' i ≤ 1,
-  { simp_rw [f', g', div_mul_div, ← sum_div] at this,
+  { simp_rw [f', g', div_mul_div_comm₀, ← sum_div] at this,
     rwa [div_le_iff, one_mul] at this,
     refine mul_ne_zero _ _,
     { rw [ne.def, rpow_eq_zero_iff, not_and_distrib], exact or.inl hF_zero, },

src/analysis/special_functions/polynomials.lean

@@ -141,7 +141,7 @@ begin
   refine (P.is_equivalent_at_top_lead.symm.div
           Q.is_equivalent_at_top_lead.symm).symm.trans
          (eventually_eq.is_equivalent ((eventually_gt_at_top 0).mono $ λ x hx, _)),
-  simp [← div_mul_div, hP, hQ, zpow_sub₀ hx.ne.symm]
+  simp [← div_mul_div_comm₀, hP, hQ, zpow_sub₀ hx.ne.symm]
 end
 
 lemma div_tendsto_zero_of_degree_lt (hdeg : P.degree < Q.degree) :

src/analysis/special_functions/trigonometric/complex.lean

@@ -107,7 +107,7 @@ begin
         ← div_div_div_cancel_right (sin x * cos y + cos x * sin y)
             (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
         add_div, sub_div],
-    simp only [←div_mul_div, ←tan, mul_one, one_mul,
+    simp only [←div_mul_div_comm₀, ←tan, mul_one, one_mul,
               div_self (cos_ne_zero_iff.mpr h1), div_self (cos_ne_zero_iff.mpr h2)] },
   { obtain ⟨t, hx, hy, hxy⟩ := ⟨tan_int_mul_pi_div_two, t (2*k+1), t (2*l+1), t (2*k+1+(2*l+1))⟩,
     simp only [int.cast_add, int.cast_bit0, int.cast_mul, int.cast_one, hx, hy] at hx hy hxy,

src/analysis/specific_limits.lean

@@ -1108,7 +1108,7 @@ begin
   -- Finally, we prove the upper estimate
   intros n hn,
   calc ∥x ^ (n + 1) / (n + 1)!∥ = (∥x∥ / (n + 1)) * ∥x ^ n / n!∥ :
-    by rw [pow_succ, nat.factorial_succ, nat.cast_mul, ← div_mul_div,
+    by rw [pow_succ, nat.factorial_succ, nat.cast_mul, ← div_mul_div_comm₀,
       norm_mul, norm_div, real.norm_coe_nat, nat.cast_succ]
   ... ≤ (∥x∥ / (⌊∥x∥⌋₊ + 1)) * ∥x ^ n / n!∥ :
     by mono* with [0 ≤ ∥x ^ n / n!∥, 0 ≤ ∥x∥]; apply norm_nonneg