feat: port Algebra.Hom.Group (#659)

mathlib3 SHA: 8c53048add6ffacdda0b36c4917bfe37e209b0ba

- [x] depends on #563
- [x] depends on leanprover-community/mathlib3#17733
- [x] depends on leanprover/lean4#1901
- [x] depends on leanprover/lean4#1907

Co-authored-by: Winston Yin <winstonyin@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib.lean

@@ -21,6 +21,7 @@ import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.HierarchyDesign
 import Mathlib.Algebra.Hom.Embedding
+import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites

Mathlib/Algebra/Group/Defs.lean

@@ -783,10 +783,16 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
     _ = a * a ^ n := congr_arg ((· * ·) a) (zpow_ofNat a n)
     _ = a ^ (n + 1) := (pow_succ _ _).symm
 
-@[simp, to_additive]
+@[simp]
 theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
   rw [← zpow_ofNat]
   exact DivInvMonoid.zpow_neg' n a
+@[simp]
+theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) :
+  Int.negSucc n • a = -((n + 1) • a) := by
+  rw [← ofNat_zsmul]
+  exact SubNegMonoid.zsmul_neg' n a
+attribute [to_additive negSucc_zsmul] zpow_negSucc
 
 /-- Dividing by an element is the same as multiplying by its inverse.