feat(Algebra/GroupRingAction/Basic): RingHom application forms a `M…

…ulDistribMulAction` (#8396)

This replaces a previous weaker result that it formed a `DistribMulAction`.

The docstring seemed to assume this already existed, but forgot to mention the `RingAut` version in another file.

Mathlib/Algebra/GroupRingAction/Basic.lean

@@ -66,6 +66,29 @@ theorem toRingHom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
   eq_of_smul_eq_smul fun r => RingHom.ext_iff.1 h r
 #align to_ring_hom_injective toRingHom_injective
 
+/-- The tautological action by `R →+* R` on `R`.
+
+This generalizes `Function.End.applyMulAction`. -/
+instance RingHom.applyMulSemiringAction [Semiring R] : MulSemiringAction (R →+* R) R where
+  smul := (· <| ·)
+  smul_one := map_one
+  smul_mul := map_mul
+  smul_zero := RingHom.map_zero
+  smul_add := RingHom.map_add
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+#align ring_hom.apply_distrib_mul_action RingHom.applyMulSemiringActionₓ
+
+@[simp]
+protected theorem RingHom.smul_def [Semiring R] (f : R →+* R) (a : R) : f • a = f a :=
+  rfl
+#align ring_hom.smul_def RingHom.smul_def
+
+/-- `RingHom.applyMulSemiringAction` is faithful. -/
+instance RingHom.applyFaithfulSMul [Semiring R] : FaithfulSMul (R →+* R) R :=
+  ⟨fun {_ _} h => RingHom.ext h⟩
+#align ring_hom.apply_has_faithful_smul RingHom.applyFaithfulSMul
+
 /-- Each element of the group defines a semiring isomorphism. -/
 @[simps!]
 def MulSemiringAction.toRingEquiv [MulSemiringAction G R] (x : G) : R ≃+* R :=

Mathlib/Algebra/Module/Basic.lean

@@ -358,27 +358,6 @@ def RingHom.toModule [Semiring R] [Semiring S] (f : R →+* S) : Module R S :=
   Module.compHom S f
 #align ring_hom.to_module RingHom.toModule
 
-/-- The tautological action by `R →+* R` on `R`.
-
-This generalizes `Function.End.applyMulAction`. -/
-instance RingHom.applyDistribMulAction [Semiring R] : DistribMulAction (R →+* R) R where
-  smul := (· <| ·)
-  smul_zero := RingHom.map_zero
-  smul_add := RingHom.map_add
-  one_smul _ := rfl
-  mul_smul _ _ _ := rfl
-#align ring_hom.apply_distrib_mul_action RingHom.applyDistribMulAction
-
-@[simp]
-protected theorem RingHom.smul_def [Semiring R] (f : R →+* R) (a : R) : f • a = f a :=
-  rfl
-#align ring_hom.smul_def RingHom.smul_def
-
-/-- `RingHom.applyDistribMulAction` is faithful. -/
-instance RingHom.applyFaithfulSMul [Semiring R] : FaithfulSMul (R →+* R) R :=
-  ⟨fun {_ _} h => RingHom.ext h⟩
-#align ring_hom.apply_has_faithful_smul RingHom.applyFaithfulSMul
-
 section AddCommMonoid
 
 variable [Semiring R] [AddCommMonoid M] [Module R M]

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -1124,10 +1124,10 @@ This is generalized to bundled endomorphisms by:
 * `AddMonoid.End.applyModule`
 * `AddAut.applyDistribMulAction`
 * `MulAut.applyMulDistribMulAction`
-* `RingHom.applyDistribMulAction`
 * `LinearEquiv.applyDistribMulAction`
 * `LinearMap.applyModule`
 * `RingHom.applyMulSemiringAction`
+* `RingAut.applyMulSemiringAction`
 * `AlgEquiv.applyMulSemiringAction`
 -/
 instance Function.End.applyMulAction :