chore: Delete Algebra.GroupPower.Ring (#12957)

Move the few remaining lemmas to earlier files.

Author: YaelDillies

Mathlib.lean

@@ -252,7 +252,6 @@ import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupPower.Order
-import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Conj

Mathlib/Algebra/GroupPower/Ring.lean

@@ -140,7 +140,7 @@ end MonoidWithZero
 
 section CancelCommMonoidWithZero
 
-variable [CancelCommMonoidWithZero α] [Subsingleton αˣ] {a b : α}
+variable [CancelCommMonoidWithZero α] [Subsingleton αˣ] {a b : α} {m n : ℕ}
 
 theorem dvd_antisymm : a ∣ b → b ∣ a → a = b := by
   rintro ⟨c, rfl⟩ ⟨d, hcd⟩
@@ -169,4 +169,18 @@ theorem eq_of_forall_dvd' (h : ∀ c, c ∣ a ↔ c ∣ b) : a = b :=
   ((h _).1 dvd_rfl).antisymm <| (h _).2 dvd_rfl
 #align eq_of_forall_dvd' eq_of_forall_dvd'
 
+lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ n ≤ m := by
+  constructor
+  · intro h
+    rw [← not_lt]
+    intro hmn
+    apply ha
+    have : a ^ m * a ∣ a ^ m * 1 := by
+      rw [← pow_succ, mul_one]
+      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
+    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
+    apply pow_ne_zero m ha₀
+  · apply pow_dvd_pow
+#align pow_dvd_pow_iff pow_dvd_pow_iff
+
 end CancelCommMonoidWithZero

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.NeZero
 
 #align_import algebra.hom.group from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
@@ -39,7 +39,7 @@ assert_not_exists DenselyOrdered
 open Function
 
 namespace NeZero
-variable {F α β  : Type*} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α}
+variable {F α β : Type*} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α}
 
 lemma of_map (f : F) [neZero : NeZero (f a)] : NeZero a :=
   ⟨fun h ↦ ne (f a) <| by rw [h]; exact ZeroHomClass.map_zero f⟩
@@ -51,7 +51,7 @@ lemma of_injective {f : F} (hf : Injective f) [NeZero a] : NeZero (f a) :=
 
 end NeZero
 
-variable {F α β γ δ : Type*} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ]
+variable {F α β γ δ M₀ : Type*} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ]
   [MulZeroOneClass δ]
 
 /-- `MonoidWithZeroHomClass F α β` states that `F` is a type of
@@ -260,6 +260,22 @@ instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
 
 end MonoidWithZeroHom
 
+section CommMonoidWithZero
+variable [CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0)
+
+/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `MonoidWithZeroHom` -/
+def powMonoidWithZeroHom : M₀ →*₀ M₀ :=
+  { powMonoidHom n with map_zero' := zero_pow hn }
+#align pow_monoid_with_zero_hom powMonoidWithZeroHom
+
+@[simp] lemma coe_powMonoidWithZeroHom : (powMonoidWithZeroHom hn : M₀ → M₀) = fun x ↦ x ^ n := rfl
+#align coe_pow_monoid_with_zero_hom coe_powMonoidWithZeroHom
+
+@[simp] lemma powMonoidWithZeroHom_apply (a : M₀) : powMonoidWithZeroHom hn a = a ^ n := rfl
+#align pow_monoid_with_zero_hom_apply powMonoidWithZeroHom_apply
+
+end CommMonoidWithZero
+
 /-! ### Equivalences -/
 
 namespace MulEquivClass

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 import Mathlib.Algebra.Algebra.Tower
+import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Regular.Pow
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Data.Finsupp.Antidiagonal

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import Mathlib.Algebra.Field.Defs
-import Mathlib.Algebra.GroupWithZero.Units.Basic
+import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Order.Ring.Defs
 
 #align_import algebra.order.field.defs from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"

Mathlib/Algebra/Order/Field/Defs.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Data.Finset.Sort
 

Mathlib/Algebra/Polynomial/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.GroupTheory.GroupAction.Ring

Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Mario Carneiro
 -/
 import Mathlib.Algebra.CharZero.Lemmas
+import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Image
 

Mathlib/Data/Complex/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.WithTop
+import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Data.ENNReal.Basic
 
 #align_import data.real.ennreal from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"