chore(group_theory/group_action/group): add smul_inv (#7568)

This renames the existing `smul_inv` to `smul_inv'`, which is consistent with the name of the other lemma about `mul_semiring_action`, `smul_mul'`.

src/algebra/group_ring_action.lean

@@ -113,7 +113,7 @@ variables {M G A R}
 
 attribute [simp] smul_one smul_mul' smul_zero smul_add
 
-@[simp] lemma smul_inv [mul_semiring_action M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹ :=
+@[simp] lemma smul_inv' [mul_semiring_action M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹ :=
 (mul_semiring_action.to_semiring_hom M F x).map_inv _
 
 @[simp] lemma smul_pow [mul_semiring_action M R] (x : M) (m : R) (n : ℕ) :

src/field_theory/fixed.lean

@@ -42,7 +42,7 @@ instance fixed_by.is_subfield : is_subfield (fixed_by G F g) :=
   neg_mem := λ x hx, (smul_neg g x).trans $ congr_arg _ hx,
   one_mem := smul_one g,
   mul_mem := λ x y hx hy, (smul_mul' g x y).trans $ congr_arg2 _ hx hy,
-  inv_mem := λ x hx, (smul_inv F g x).trans $ congr_arg _ hx }
+  inv_mem := λ x hx, (smul_inv' F g x).trans $ congr_arg _ hx }
 
 namespace fixed_points
 

src/field_theory/galois.lean

@@ -188,7 +188,7 @@ def fixed_field : intermediate_field F E :=
   neg_mem' := λ a hx g, by rw [smul_neg g a, hx],
   one_mem' := λ g, smul_one g,
   mul_mem' := λ a b hx hy g, by rw [smul_mul' g a b, hx, hy],
-  inv_mem' := λ a hx g, by rw [smul_inv _ g a, hx],
+  inv_mem' := λ a hx g, by rw [smul_inv' _ g a, hx],
   algebra_map_mem' := λ a g, commutes g a }
 
 lemma finrank_fixed_field_eq_card [finite_dimensional F E] :

src/group_theory/group_action/group.lean

@@ -102,6 +102,10 @@ variables [group α] [mul_action α β]
 @[to_additive] lemma eq_inv_smul_iff {a : α} {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
 (to_units a).smul_perm.eq_symm_apply
 
+lemma smul_inv [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
+  (c • x)⁻¹ = c⁻¹ • x⁻¹ :=
+by rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]
+
 variables (α) (β)
 
 /-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/