feat(algebra/group/commute): div lemmas (#18607)

`commute` analogs of existing lemmas. Also normalise lemma names about `commute` and `nat.cast`/`int.cast`, following existing `int.cast` lemmas.

src/algebra/field/basic.lean

@@ -6,7 +6,7 @@ Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 import algebra.field.defs
 import algebra.group_with_zero.units.lemmas
 import algebra.hom.ring
-import algebra.ring.inj_surj
+import algebra.ring.commute
 
 /-!
 # Lemmas about division (semi)rings and (semi)fields
@@ -24,7 +24,7 @@ universe u
 variables {α β K : Type*}
 
 section division_semiring
-variables [division_semiring α] {a b c : α}
+variables [division_semiring α] {a b c d : α}
 
 lemma add_div (a b c : α) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
 
@@ -50,6 +50,18 @@ by rw [add_div, mul_div_cancel _ hc]
 @[field_simps] lemma div_add' (a b c : α) (hc : c ≠ 0) : a / c + b = (a + b * c) / c :=
 by rwa [add_comm, add_div', add_comm]
 
+protected lemma commute.div_add_div (hbc : commute b c) (hbd : commute b d) (hb : b ≠ 0)
+  (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d) :=
+by rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
+
+protected lemma commute.one_div_add_one_div (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
+  1 / a + 1 / b = (a + b) / (a * b) :=
+by rw [(commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
+
+protected lemma commute.inv_add_inv (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
+  a⁻¹ + b⁻¹ = (a + b) / (a * b) :=
+by rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
+
 end division_semiring
 
 section division_monoid
@@ -94,7 +106,7 @@ by rw neg_inv
 end division_monoid
 
 section division_ring
-variables [division_ring K] {a b : K}
+variables [division_ring K] {a b c d : K}
 
 @[simp] lemma div_neg_self {a : K} (h : a ≠ 0) : a / -a = -1 :=
 by rw [div_neg_eq_neg_div, div_self h]
@@ -131,20 +143,28 @@ by rw [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel ha), mul_sub_right_di
 instance division_ring.is_domain : is_domain K :=
 no_zero_divisors.to_is_domain _
 
+protected lemma commute.div_sub_div (hbc : commute b c) (hbd : commute b d) (hb : b ≠ 0)
+  (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d) :=
+by simpa only [mul_neg, neg_div, ←sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd
+
+protected lemma commute.inv_sub_inv (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
+  a⁻¹ - b⁻¹ = (b - a) / (a * b) :=
+by simp only [inv_eq_one_div, (commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]
+
 end division_ring
 
 section semifield
 variables [semifield α] {a b c d : α}
 
 lemma div_add_div (a : α) (c : α) (hb : b ≠ 0) (hd : d ≠ 0) :
   (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
-by rw [← mul_div_mul_right _ b hd, ← mul_div_mul_left c d hb, div_add_div_same]
+(commute.all b _).div_add_div (commute.all _ _) hb hd
 
 lemma one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
-by rw [div_add_div _ _ ha hb, one_mul, mul_one, add_comm]
+(commute.all a _).one_div_add_one_div ha hb
 
 lemma inv_add_inv (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b) :=
-by rw [inv_eq_one_div, inv_eq_one_div, one_div_add_one_div ha hb]
+(commute.all a _).inv_add_inv ha hb
 
 end semifield
 
@@ -156,14 +176,10 @@ local attribute [simp] mul_assoc mul_comm mul_left_comm
 
 @[field_simps] lemma div_sub_div (a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) :
   (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
-begin
-  simp [sub_eq_add_neg],
-  rw [neg_eq_neg_one_mul, ← mul_div_assoc, div_add_div _ _ hb hd,
-      ← mul_assoc, mul_comm b, mul_assoc, ← neg_eq_neg_one_mul]
-end
+(commute.all b _).div_sub_div (commute.all _ _) hb hd
 
 lemma inv_sub_inv {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) :=
-by rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]
+(commute.all a _).inv_sub_inv ha hb
 
 @[field_simps] lemma sub_div' (a b c : K) (hc : c ≠ 0) : b - a / c = (b * c - a) / c :=
 by simpa using div_sub_div b a one_ne_zero hc

src/algebra/group/commute.lean

@@ -85,6 +85,10 @@ by simp only [mul_assoc, h.eq]
   a * (b * c) = b * (a * c) :=
 by simp only [← mul_assoc, h.eq]
 
+@[to_additive] protected lemma mul_mul_mul_comm (hbc : commute b c) (a d : S) :
+  (a * b) * (c * d) = (a * c) * (b * d) :=
+by simp only [hbc.left_comm, mul_assoc]
+
 end semigroup
 
 @[to_additive]
@@ -171,12 +175,31 @@ u.left_of_mul b a (hc.eq ▸ hu) hc.symm
 end monoid
 
 section division_monoid
-variables [division_monoid G] {a b : G}
+variables [division_monoid G] {a b c d : G}
 
-@[to_additive] lemma inv_inv : commute a b → commute a⁻¹ b⁻¹ := semiconj_by.inv_inv_symm
+@[to_additive] protected lemma inv_inv : commute a b → commute a⁻¹ b⁻¹ := semiconj_by.inv_inv_symm
 @[simp, to_additive]
 lemma inv_inv_iff : commute a⁻¹ b⁻¹ ↔ commute a b := semiconj_by.inv_inv_symm_iff
 
+@[to_additive] protected lemma mul_inv (hab : commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
+by rw [hab.eq, mul_inv_rev]
+
+@[to_additive] protected lemma inv (hab : commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
+by rw [hab.eq, mul_inv_rev]
+
+@[to_additive] protected lemma div_mul_div_comm (hbd : commute b d) (hbc : commute b⁻¹ c) :
+  a / b * (c / d) = a * c / (b * d) :=
+by simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]
+
+@[to_additive] protected lemma mul_div_mul_comm (hcd : commute c d) (hbc : commute b c⁻¹) :
+  a * b / (c * d) = a / c * (b / d) :=
+(hcd.div_mul_div_comm hbc.symm).symm
+
+@[to_additive] protected lemma div_div_div_comm (hbc : commute b c) (hbd : commute b⁻¹ d)
+  (hcd : commute c⁻¹ d) : a / b / (c / d) = a / c / (b / d) :=
+by simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
+  hbc.inv_inv.mul_mul_mul_comm]
+
 end division_monoid
 
 section group

src/algebra/group_power/lemmas.lean

@@ -758,13 +758,12 @@ h.cast_nat_mul_left n
   commute (m * a : R) (n * b : R) :=
 h.cast_nat_mul_cast_nat_mul m n
 
-@[simp] theorem self_cast_nat_mul (n : ℕ) : commute a (n * a : R) :=
-(commute.refl a).cast_nat_mul_right n
+variables (a) (m n : ℕ)
 
-@[simp] theorem cast_nat_mul_self (n : ℕ) : commute ((n : R) * a) a :=
-(commute.refl a).cast_nat_mul_left n
+@[simp] lemma self_cast_nat_mul : commute a (n * a : R) := (commute.refl a).cast_nat_mul_right n
+@[simp] lemma cast_nat_mul_self : commute ((n : R) * a) a := (commute.refl a).cast_nat_mul_left n
 
-@[simp] theorem self_cast_nat_mul_cast_nat_mul (m n : ℕ) : commute (m * a : R) (n * a : R) :=
+@[simp] theorem self_cast_nat_mul_cast_nat_mul : commute (m * a : R) (n * a : R) :=
 (commute.refl a).cast_nat_mul_cast_nat_mul m n
 
 end
@@ -792,11 +791,8 @@ h.cast_int_mul_cast_int_mul m n
 
 variables (a) (m n : ℤ)
 
-@[simp] lemma cast_int_left : commute (m : R) a :=
-by { rw [← mul_one (m : R)], exact (one_left a).cast_int_mul_left m }
-
-@[simp] lemma cast_int_right : commute a m :=
-by { rw [← mul_one (m : R)], exact (one_right a).cast_int_mul_right m }
+@[simp] lemma cast_int_left : commute (m : R) a := int.cast_commute _ _
+@[simp] lemma cast_int_right : commute a m := int.commute_cast _ _
 
 @[simp] theorem self_cast_int_mul : commute a (n * a : R) := (commute.refl a).cast_int_mul_right n