refactor(group_theory/subgroup): swap mul_mem_cancel_left/right (#3011

)

This way the name follows the position of the term we cancel.

src/deprecated/subgroup.lean

@@ -155,11 +155,11 @@ lemma inv_mem_iff : a⁻¹ ∈ s ↔ a ∈ s :=
 ⟨λ h, by simpa using inv_mem h, inv_mem⟩
 
 @[to_additive]
-lemma mul_mem_cancel_left (h : a ∈ s) : b * a ∈ s ↔ b ∈ s :=
+lemma mul_mem_cancel_right (h : a ∈ s) : b * a ∈ s ↔ b ∈ s :=
 ⟨λ hba, by simpa using mul_mem hba (inv_mem h), λ hb, mul_mem hb h⟩
 
 @[to_additive]
-lemma mul_mem_cancel_right (h : a ∈ s) : a * b ∈ s ↔ b ∈ s :=
+lemma mul_mem_cancel_left (h : a ∈ s) : a * b ∈ s ↔ b ∈ s :=
 ⟨λ hab, by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩
 
 end is_subgroup
@@ -280,8 +280,8 @@ instance normalizer_is_subgroup (s : set G) : is_subgroup (normalizer s) :=
 
 @[to_additive subset_add_normalizer]
 lemma subset_normalizer (s : set G) [is_subgroup s] : s ⊆ normalizer s :=
-λ g hg n, by rw [is_subgroup.mul_mem_cancel_left _ ((is_subgroup.inv_mem_iff _).2 hg),
-  is_subgroup.mul_mem_cancel_right _ hg]
+λ g hg n, by rw [is_subgroup.mul_mem_cancel_right _ ((is_subgroup.inv_mem_iff _).2 hg),
+  is_subgroup.mul_mem_cancel_left _ hg]
 
 /-- Every subgroup is a normal subgroup of its normalizer -/
 @[to_additive add_normal_in_add_normalizer]

src/group_theory/coset.lean

@@ -117,11 +117,11 @@ variables [group α] (s : set α) [is_subgroup s]
 
 @[to_additive left_add_coset_mem_left_add_coset]
 lemma left_coset_mem_left_coset {a : α} (ha : a ∈ s) : a *l s = s :=
-set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_right s (inv_mem ha)]
+set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_left s (inv_mem ha)]
 
 @[to_additive right_add_coset_mem_right_add_coset]
 lemma right_coset_mem_right_coset {a : α} (ha : a ∈ s) : s *r a = s :=
-set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_left s (inv_mem ha)]
+set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_right s (inv_mem ha)]
 
 @[to_additive normal_of_eq_add_cosets]
 theorem normal_of_eq_cosets [normal_subgroup s] (g : α) : g *l s = s *r g :=

src/group_theory/order_of_element.lean

@@ -328,7 +328,7 @@ if hx : ∃ (x : α), x ∈ H ∧ x ≠ (1 : α) then
       have hk₂ : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) ∈ H,
         by rw gpow_mul; exact is_subgroup.gpow_mem (nat.find_spec hex).2,
       have hk₃ : g ^ (k % nat.find hex) ∈ H,
-        from (is_subgroup.mul_mem_cancel_left H hk₂).1 $
+        from (is_subgroup.mul_mem_cancel_right H hk₂).1 $
           by rw [← gpow_add, int.mod_add_div, hk]; exact hx,
       have hk₄ : k % nat.find hex = (k % nat.find hex).nat_abs,
         by rw int.nat_abs_of_nonneg (int.mod_nonneg _

src/group_theory/quotient_group.lean

@@ -18,7 +18,7 @@ instance : group (quotient N) :=
 { one := (1 : G),
   mul := quotient.map₂' (*)
   (λ a₁ b₁ hab₁ a₂ b₂ hab₂,
-    ((is_subgroup.mul_mem_cancel_left N (is_subgroup.inv_mem hab₂)).1
+    ((is_subgroup.mul_mem_cancel_right N (is_subgroup.inv_mem hab₂)).1
         (by rw [mul_inv_rev, mul_inv_rev, ← mul_assoc (a₂⁻¹ * a₁⁻¹),
           mul_assoc _ b₂, ← mul_assoc b₂, mul_inv_self, one_mul, mul_assoc (a₂⁻¹)];
           exact normal_subgroup.normal _ hab₁ _))),

src/group_theory/subgroup.lean

@@ -208,12 +208,15 @@ theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H := λ hx hy, H.m
 @[to_additive "An `add_subgroup` is closed under inverse."]
 theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H := λ hx, H.inv_mem' hx
 
+@[simp, to_additive] theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
+⟨λ h, inv_inv x ▸ H.inv_mem h, H.inv_mem⟩
+
 @[to_additive]
-lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
+lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
 ⟨λ hba, by simpa using H.mul_mem hba (H.inv_mem h), λ hb, H.mul_mem hb h⟩
 
 @[to_additive]
-lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
+lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
 ⟨λ hab, by simpa using H.mul_mem (H.inv_mem h) hab, H.mul_mem h⟩
 
 /-- Product of a list of elements in a subgroup is in the subgroup. -/
@@ -664,7 +667,7 @@ variable {H}
   g ∈ normalizer H ↔ ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H := iff.rfl
 
 @[to_additive] lemma le_normalizer : H ≤ normalizer H :=
-λ x xH n, by rw [H.mul_mem_cancel_left (H.inv_mem xH), H.mul_mem_cancel_right xH]
+λ x xH n, by rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]
 
 @[instance, priority 100, to_additive]
 lemma normal_in_normalizer : (H.comap H.normalizer.subtype).normal :=

src/group_theory/sylow.lean

@@ -182,7 +182,7 @@ lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : set G} [is_subgro
 (mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2
   (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in
   have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂,
-  (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_right H (inv_mem hb₁)).1
+  (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_left H (inv_mem hb₁)).1
   $ by rw hx at hb₂;
     simpa [mul_inv_rev, mul_assoc] using hb₂)⟩