Feat(Algebra/Regular/SMul): Add some lemmas about IsSMulRegular (#13123)

Add some lemmas about `IsSMulRegular`.

Author: Shamrock-Frost

Mathlib/Algebra/Regular/SMul.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.SMulWithZero
 import Mathlib.Algebra.Regular.Basic
+import Mathlib.GroupTheory.GroupAction.Hom
 
 #align_import algebra.regular.smul from "leanprover-community/mathlib"@"550b58538991c8977703fdeb7c9d51a5aa27df11"
 
@@ -122,6 +122,12 @@ theorem mul_and_mul_iff [Mul R] [IsScalarTower R R M] :
     exact ⟨ha.mul hb, hb.mul ha⟩
 #align is_smul_regular.mul_and_mul_iff IsSMulRegular.mul_and_mul_iff
 
+lemma isSMulRegular_of_injective_of_isSMulRegular {N F} [SMul R N]
+    [FunLike F M N] [MulActionHomClass F R M N] (f : F) {r : R}
+    (h1 : Function.Injective f) (h2 : IsSMulRegular N r) : IsSMulRegular M r :=
+    fun x y h3 => h1 <| h2 <| (map_smulₛₗ f r x).symm.trans <|
+      (congrArg f h3).trans <| map_smulₛₗ f r y
+
 end SMul
 
 section Monoid
@@ -255,3 +261,20 @@ theorem IsUnit.isSMulRegular (ua : IsUnit a) : IsSMulRegular M a := by
 #align is_unit.is_smul_regular IsUnit.isSMulRegular
 
 end Units
+
+section SMulZeroClass
+
+variable {M}
+
+protected
+lemma IsSMulRegular.eq_zero_of_smul_eq_zero [Zero M] [SMulZeroClass R M]
+    {r : R} {x : M} (h1 : IsSMulRegular M r) (h2 : r • x = 0) : x = 0 :=
+  h1 (h2.trans (smul_zero r).symm)
+
+end SMulZeroClass
+
+lemma Equiv.isSMulRegular_congr {R S M M'} [SMul R M] [SMul S M'] {e : M ≃ M'}
+    {r : R} {s : S} (h : ∀ x, e (r • x) = s • e x) :
+    IsSMulRegular M r ↔ IsSMulRegular M' s :=
+  (e.comp_injective _).symm.trans  <|
+    (iff_of_eq <| congrArg _ <| funext h).trans <| e.injective_comp _