chore: Move MulOpposite.op_pow (#9442)

These lemmas can actually be proved much earlier than they were.

Part of #9411

Mathlib/Algebra/Group/Opposite.lean

@@ -181,6 +181,29 @@ instance commGroup [CommGroup α] : CommGroup αᵐᵒᵖ :=
   { MulOpposite.group α, MulOpposite.commMonoid α with }
 
 variable {α}
+
+section Monoid
+variable [Monoid α]
+
+@[simp] lemma op_pow (x : α) (n : ℕ) : op (x ^ n) = op x ^ n := rfl
+#align mul_opposite.op_pow MulOpposite.op_pow
+
+@[simp] lemma unop_pow (x : αᵐᵒᵖ) (n : ℕ) : unop (x ^ n) = unop x ^ n := rfl
+#align mul_opposite.unop_pow MulOpposite.unop_pow
+
+end Monoid
+
+section DivInvMonoid
+variable [DivInvMonoid α]
+
+@[simp] lemma op_zpow (x : α) (z : ℤ) : op (x ^ z) = op x ^ z := rfl
+#align mul_opposite.op_zpow MulOpposite.op_zpow
+
+@[simp] lemma unop_zpow (x : αᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = unop x ^ z := rfl
+#align mul_opposite.unop_zpow MulOpposite.unop_zpow
+
+end DivInvMonoid
+
 @[to_additive (attr := simp, norm_cast)]
 theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n :=
   rfl

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -1218,32 +1218,6 @@ theorem conj_pow' (u : Mˣ) (x : M) (n : ℕ) :
 
 end Units
 
-namespace MulOpposite
-
-/-- Moving to the opposite monoid commutes with taking powers. -/
-@[simp]
-theorem op_pow [Monoid M] (x : M) (n : ℕ) : op (x ^ n) = op x ^ n :=
-  rfl
-#align mul_opposite.op_pow MulOpposite.op_pow
-
-@[simp]
-theorem unop_pow [Monoid M] (x : Mᵐᵒᵖ) (n : ℕ) : unop (x ^ n) = unop x ^ n :=
-  rfl
-#align mul_opposite.unop_pow MulOpposite.unop_pow
-
-/-- Moving to the opposite group or `GroupWithZero` commutes with taking powers. -/
-@[simp]
-theorem op_zpow [DivInvMonoid M] (x : M) (z : ℤ) : op (x ^ z) = op x ^ z :=
-  rfl
-#align mul_opposite.op_zpow MulOpposite.op_zpow
-
-@[simp]
-theorem unop_zpow [DivInvMonoid M] (x : Mᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = unop x ^ z :=
-  rfl
-#align mul_opposite.unop_zpow MulOpposite.unop_zpow
-
-end MulOpposite
-
 -- Porting note: this was added in an ad hoc port for use in `Tactic/NormNum/Basic`
 
 @[simp] theorem pow_eq {m : ℤ} {n : ℕ} : m.pow n = m ^ n := rfl