chore(GroupTheory): deduplicate RootableBy.surjective_pow (#38252)

[pow_left_surj_of_rootableBy](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Divisible.html#pow_left_surj_of_rootableBy) and [RootableBy.surjective_pow](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Divisible.html#RootableBy.surjective_pow) have the same statement, so this PR deprecates one of them. I kept the one with better naming (`surj` is not a widely used abbrev)

Author: wwylele

Mathlib/GroupTheory/Divisible.lean

@@ -110,11 +110,17 @@ class RootableBy where
   root_zero : ∀ a, root a 0 = 1
   root_cancel : ∀ {n : α} (a : A), n ≠ 0 → root a n ^ n = a
 
-@[to_additive smul_right_surj_of_divisibleBy]
-theorem pow_left_surj_of_rootableBy [RootableBy A α] {n : α} (hn : n ≠ 0) :
-    Function.Surjective (fun a => a ^ n : A → A) := fun x =>
+@[to_additive DivisibleBy.surjective_smul]
+theorem RootableBy.surjective_pow [RootableBy A α] {n : α} (hn : n ≠ 0) :
+    Function.Surjective fun a : A => a ^ n := fun x =>
   ⟨RootableBy.root x n, RootableBy.root_cancel _ hn⟩
 
+@[deprecated (since := "2026-04-19")] alias pow_left_surj_of_rootableBy :=
+  RootableBy.surjective_pow
+
+@[deprecated (since := "2026-04-19")] alias smul_right_surj_of_divisibleBy :=
+  DivisibleBy.surjective_smul
+
 /--
 A `Monoid A` is `α`-rootable iff the `pow _ n` function is surjective, i.e. the constructive version
 implies the textbook approach.
@@ -252,11 +258,6 @@ noncomputable def Function.Surjective.rootableBy (hf : Function.Surjective f)
     ⟨f <| RootableBy.root y n,
       (by rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy] : _ ^ n = x)⟩
 
-@[to_additive DivisibleBy.surjective_smul]
-theorem RootableBy.surjective_pow (A α : Type*) [Monoid A] [Pow A α] [Zero α] [RootableBy A α]
-    {n : α} (hn : n ≠ 0) : Function.Surjective fun a : A => a ^ n := fun a =>
-  ⟨RootableBy.root a n, RootableBy.root_cancel a hn⟩
-
 end Hom
 
 section Quotient