chore(algebra/group_power/basic): reduce imports (#17334)

* [after.pdf](https://leanprover.zulipchat.com/user_uploads/3121/R1Gg-EUylJs9H_GH1ERnKAX4/after.pdf)
* [before.pdf](https://leanprover.zulipchat.com/user_uploads/user_uploads/3121/xYgoBBhTlgAaD_boJtN6ZHHO/before.pdf)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/divisibility.lean

@@ -145,6 +145,10 @@ mul_dvd_mul (dvd_refl a) h
 theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
 mul_dvd_mul h (dvd_refl c)
 
+theorem pow_dvd_pow_of_dvd {a b : α} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
+| 0     := by rw [pow_zero, pow_zero]
+| (n+1) := by { rw [pow_succ, pow_succ], exact mul_dvd_mul h (pow_dvd_pow_of_dvd n) }
+
 end comm_monoid
 
 section semigroup_with_zero

src/algebra/group_power/basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.divisibility
-import algebra.group.commute
 import algebra.group.type_tags
-import data.nat.basic
 
 /-!
 # Power operations on monoids and groups
@@ -118,7 +116,7 @@ by rw [←pow_add, nat.sub_add_cancel h]
 lemma pow_eq_pow_mod {M : Type*} [monoid M] {x : M} (m : ℕ) {n : ℕ} (h : x ^ n = 1) :
   x ^ m = x ^ (m % n) :=
 begin
-  have t := congr_arg (λ a, x ^ a) (nat.div_add_mod m n).symm,
+  have t := congr_arg (λ a, x ^ a) ((nat.add_comm _ _).trans (nat.mod_add_div _ _)).symm,
   dsimp at t,
   rw [t, pow_add, pow_mul, h, one_pow, one_mul],
 end
@@ -301,10 +299,6 @@ end group
 lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :
   a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, nat.sub_add_cancel h]⟩
 
-theorem pow_dvd_pow_of_dvd [comm_monoid R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
-| 0     := by rw [pow_zero, pow_zero]
-| (n+1) := by { rw [pow_succ, pow_succ], exact mul_dvd_mul h (pow_dvd_pow_of_dvd n) }
-
 lemma of_add_nsmul [add_monoid A] (x : A) (n : ℕ) :
   multiplicative.of_add (n • x) = (multiplicative.of_add x)^n := rfl
 

src/algebra/hom/group_instances.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
   Johannes Hölzl, Yury Kudryashov
 -/
-
 import algebra.group_power.basic
+import algebra.ring.basic
 
 /-!
 # Instances on spaces of monoid and group morphisms