chore(algebra/group/prod): prod.swap commutes with arithmetic (#12367)

This also adds some missing `div` lemmas using `to_additive`.

Author: eric-wieser

src/algebra/group/prod.lean

@@ -42,6 +42,8 @@ lemma snd_mul [has_mul M] [has_mul N] (p q : M × N) : (p * q).2 = p.2 * q.2 :=
 @[simp, to_additive]
 lemma mk_mul_mk [has_mul M] [has_mul N] (a₁ a₂ : M) (b₁ b₂ : N) :
   (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂) := rfl
+@[simp, to_additive]
+lemma swap_mul [has_mul M] [has_mul N] (p q : M × N) : (p * q).swap = p.swap * q.swap := rfl
 @[to_additive]
 lemma mul_def [has_mul M] [has_mul N] (p q : M × N) : p * q = (p.1 * q.1, p.2 * q.2) := rfl
 
@@ -57,6 +59,8 @@ lemma one_eq_mk [has_one M] [has_one N] : (1 : M × N) = (1, 1) := rfl
 @[simp, to_additive]
 lemma mk_eq_one [has_one M] [has_one N] {x : M} {y : N} : (x, y) = 1 ↔ x = 1 ∧ y = 1 :=
 mk.inj_iff
+@[simp, to_additive]
+lemma swap_one [has_one M] [has_one N] : (1 : M × N).swap = 1 := rfl
 
 @[to_additive]
 lemma fst_mul_snd [mul_one_class M] [mul_one_class N] (p : M × N) :
@@ -72,14 +76,18 @@ lemma fst_inv [has_inv G] [has_inv H] (p : G × H) : (p⁻¹).1 = (p.1)⁻¹ :=
 lemma snd_inv [has_inv G] [has_inv H] (p : G × H) : (p⁻¹).2 = (p.2)⁻¹ := rfl
 @[simp, to_additive]
 lemma inv_mk [has_inv G] [has_inv H] (a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹) := rfl
+@[simp, to_additive]
+lemma swap_inv [has_inv G] [has_inv H] (p : G × H) : (p⁻¹).swap = p.swap⁻¹ := rfl
 
 @[to_additive]
 instance [has_div M] [has_div N] : has_div (M × N) := ⟨λ p q, ⟨p.1 / q.1, p.2 / q.2⟩⟩
 
-@[simp] lemma fst_sub [add_group A] [add_group B] (a b : A × B) : (a - b).1 = a.1 - b.1 := rfl
-@[simp] lemma snd_sub [add_group A] [add_group B] (a b : A × B) : (a - b).2 = a.2 - b.2 := rfl
-@[simp] lemma mk_sub_mk [add_group A] [add_group B] (x₁ x₂ : A) (y₁ y₂ : B) :
-(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂) := rfl
+@[simp, to_additive] lemma fst_div [group G] [group H] (a b : G × H) : (a / b).1 = a.1 / b.1 := rfl
+@[simp, to_additive] lemma snd_div [group G] [group H] (a b : G × H) : (a / b).2 = a.2 / b.2 := rfl
+@[simp, to_additive] lemma mk_div_mk [group G] [group H] (x₁ x₂ : G) (y₁ y₂ : H) :
+  (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂) := rfl
+@[simp, to_additive] lemma swap_div [group G] [group H] (a b : G × H) :
+  (a / b).swap = a.swap / b.swap := rfl
 
 instance [mul_zero_class M] [mul_zero_class N] : mul_zero_class (M × N) :=
 { zero_mul := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨zero_mul _, zero_mul _⟩,

src/group_theory/group_action/prod.lean

@@ -32,6 +32,7 @@ variables [has_scalar M α] [has_scalar M β] [has_scalar N α] [has_scalar N β
 @[simp, to_additive] theorem smul_snd : (a • x).2 = a • x.2 := rfl
 @[simp, to_additive] theorem smul_mk (a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c) := rfl
 @[to_additive] theorem smul_def (a : M) (x : α × β) : a • x = (a • x.1, a • x.2) := rfl
+@[simp, to_additive] theorem smul_swap : (a • x).swap = a • x.swap := rfl
 
 instance [has_scalar M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
   is_scalar_tower M N (α × β) :=