diff --git a/Mathlib.lean b/Mathlib.lean
index ec9840be5283e0..ab9f53247c7e6c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -296,6 +296,7 @@ import Mathlib.Algebra.Group.Hom.CompTypeclasses
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Group.Hom.Instances
+import Mathlib.Algebra.Group.Idempotent
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.Int.Defs
@@ -389,6 +390,7 @@ import Mathlib.Algebra.GroupWithZero.Conj
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.GroupWithZero.Hom
+import Mathlib.Algebra.GroupWithZero.Idempotent
 import Mathlib.Algebra.GroupWithZero.Indicator
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.Invertible
@@ -402,6 +404,7 @@ import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
 import Mathlib.Algebra.GroupWithZero.Prod
 import Mathlib.Algebra.GroupWithZero.Semiconj
+import Mathlib.Algebra.GroupWithZero.Submonoid
 import Mathlib.Algebra.GroupWithZero.ULift
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Equiv
@@ -905,7 +908,7 @@ import Mathlib.Algebra.Ring.Ext
 import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Algebra.Ring.Identities
 import Mathlib.Algebra.Ring.InjSurj
 import Mathlib.Algebra.Ring.Int.Defs
@@ -925,6 +928,7 @@ import Mathlib.Algebra.Ring.Rat
 import Mathlib.Algebra.Ring.Regular
 import Mathlib.Algebra.Ring.Semiconj
 import Mathlib.Algebra.Ring.Semireal.Defs
+import Mathlib.Algebra.Ring.Submonoid
 import Mathlib.Algebra.Ring.Subring.Basic
 import Mathlib.Algebra.Ring.Subring.Defs
 import Mathlib.Algebra.Ring.Subring.IntPolynomial
diff --git a/Mathlib/Algebra/Group/Idempotent.lean b/Mathlib/Algebra/Group/Idempotent.lean
new file mode 100644
index 00000000000000..af377dc9635a42
--- /dev/null
+++ b/Mathlib/Algebra/Group/Idempotent.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Group.Commute.Defs
+import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Data.Subtype
+import Mathlib.Tactic.MinImports
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `a ^ (n+1) = a` for `a` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+assert_not_exists GroupWithZero
+
+variable {M N S : Type*}
+
+/-- An element `a` is said to be idempotent if `a * a = a`. -/
+def IsIdempotentElem [Mul M] (a : M) : Prop := a * a = a
+
+namespace IsIdempotentElem
+section Mul
+variable [Mul M] {a : M}
+
+lemma of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
+  Std.IdempotentOp.idempotent a
+
+lemma eq (ha : IsIdempotentElem a) : a * a = a := ha
+
+end Mul
+
+section Semigroup
+variable [Semigroup S] {a b : S}
+
+lemma mul_of_commute (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
+    IsIdempotentElem (a * b) := by rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
+
+end Semigroup
+
+section CommSemigroup
+variable [CommSemigroup S] {a b : S}
+
+lemma mul (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b) :=
+  ha.mul_of_commute (.all ..) hb
+
+end CommSemigroup
+
+section MulOneClass
+variable [MulOneClass M] {a : M}
+
+lemma one : IsIdempotentElem (1 : M) := mul_one _
+
+instance : One {a : M // IsIdempotentElem a} where one := ⟨1, one⟩
+
+@[simp, norm_cast] lemma coe_one : ↑(1 : {a : M // IsIdempotentElem a}) = (1 : M) := rfl
+
+end MulOneClass
+
+section Monoid
+variable [Monoid M] {a : M}
+
+lemma pow (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n) :=
+  Nat.recOn n ((pow_zero a).symm ▸ one) fun n _ =>
+    show a ^ n.succ * a ^ n.succ = a ^ n.succ by
+      conv_rhs => rw [← h.eq] -- Porting note: was `nth_rw 3 [← h.eq]`
+      rw [← sq, ← sq, ← pow_mul, ← pow_mul']
+
+lemma pow_succ_eq (n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a :=
+  Nat.recOn n ((Nat.zero_add 1).symm ▸ pow_one a) fun n ih => by rw [pow_succ, ih, h.eq]
+
+end Monoid
+
+section CancelMonoid
+variable [CancelMonoid M] {a : M}
+
+@[simp] lemma iff_eq_one : IsIdempotentElem a ↔ a = 1 := by simp [IsIdempotentElem]
+
+end CancelMonoid
+
+lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M}
+    (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e) := by
+  rw [IsIdempotentElem, ← map_mul, he.eq]
+
+end IsIdempotentElem
diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean
index c0c980dcc53c08..b052c2e3e8b5a4 100644
--- a/Mathlib/Algebra/Group/Submonoid/Membership.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean
@@ -5,14 +5,11 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
+import Mathlib.Algebra.Group.Idempotent
 import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Group.Submonoid.MulOpposite
 import Mathlib.Algebra.Group.Submonoid.Operations
-import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Ring.Idempotents
-import Mathlib.Algebra.Ring.Int.Defs
 import Mathlib.Data.Fintype.Card
-import Mathlib.Data.Nat.Cast.Basic
 
 /-!
 # Submonoids: membership criteria
@@ -33,6 +30,7 @@ In this file we prove various facts about membership in a submonoid:
 submonoid, submonoids
 -/
 
+assert_not_exists MonoidWithZero
 -- We don't need ordered structures to establish basic membership facts for submonoids
 assert_not_exists OrderedSemiring
 
@@ -334,7 +332,7 @@ abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (po
     simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
     rw [Int.negSucc_coe, ← Int.add_mul_emod_self (b := (m + 1 : ℕ))]
     nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
-    rw [← sub_eq_neg_add, ← mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
+    rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
     simp only [Int.toNat_natCast]
     rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
       ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]
@@ -483,40 +481,6 @@ an additive group if that element has finite order."] Submonoid.groupPowers
 
 end AddSubmonoid
 
-/-! Lemmas about additive closures of `Subsemigroup`. -/
-
-
-namespace MulMemClass
-
-variable {R : Type*} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M}
-  {a b : R}
-
-/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
-and an element of `M` is contained in the additive closure of `M`. -/
-theorem mul_right_mem_add_closure (ha : a ∈ AddSubmonoid.closure (S : Set R)) (hb : b ∈ S) :
-    a * b ∈ AddSubmonoid.closure (S : Set R) := by
-  induction ha using AddSubmonoid.closure_induction with
-  | mem r hr => exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
-  | one => simp only [zero_mul, zero_mem _]
-  | mul r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
-
-/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
-additive closure of `M`. -/
-theorem mul_mem_add_closure (ha : a ∈ AddSubmonoid.closure (S : Set R))
-    (hb : b ∈ AddSubmonoid.closure (S : Set R)) : a * b ∈ AddSubmonoid.closure (S : Set R) := by
-  induction hb using AddSubmonoid.closure_induction with
-  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
-  | one => simp only [mul_zero, zero_mem _]
-  | mul r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
-
-/-- The product of an element of `S` and an element of the additive closure of a multiplicative
-submonoid `S` is contained in the additive closure of `S`. -/
-theorem mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ AddSubmonoid.closure (S : Set R)) :
-    a * b ∈ AddSubmonoid.closure (S : Set R) :=
-  mul_mem_add_closure (AddSubmonoid.mem_closure.mpr fun _sT hT => hT ha) hb
-
-end MulMemClass
-
 namespace Submonoid
 
 /-- An element is in the closure of a two-element set if it is a linear combination of those two
@@ -552,9 +516,3 @@ theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
   exact ofMul_image_powers_eq_multiples_ofMul
 
 end mul_add
-
-/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
-def Submonoid.isPrimal (α) [CancelCommMonoidWithZero α] : Submonoid α where
-  carrier := {a | IsPrimal a}
-  mul_mem' := IsPrimal.mul
-  one_mem' := isUnit_one.isPrimal
diff --git a/Mathlib/Algebra/GroupWithZero/Idempotent.lean b/Mathlib/Algebra/GroupWithZero/Idempotent.lean
new file mode 100644
index 00000000000000..adcc2a2df562de
--- /dev/null
+++ b/Mathlib/Algebra/GroupWithZero/Idempotent.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.Group.Idempotent
+import Mathlib.Algebra.GroupWithZero.Defs
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.one_sub_iff`: In a (non-associative) ring, `p` is an idempotent if and only if
+  `1-p` is an idempotent.
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `p ^ (n+1) = p` for `p` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+assert_not_exists Ring
+
+variable {M N S M₀ M₁ R G G₀ : Type*}
+variable [MulOneClass M₁] [CancelMonoidWithZero G₀]
+
+namespace IsIdempotentElem
+section MulZeroClass
+variable [MulZeroClass M₀]
+
+lemma zero : IsIdempotentElem (0 : M₀) := mul_zero _
+
+instance : Zero { p : M₀ // IsIdempotentElem p } where zero := ⟨0, zero⟩
+
+@[simp] lemma coe_zero : ↑(0 : { p : M₀ // IsIdempotentElem p }) = (0 : M₀) := rfl
+
+end MulZeroClass
+
+section CancelMonoidWithZero
+variable [CancelMonoidWithZero M₀]
+
+@[simp]
+lemma iff_eq_zero_or_one {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1 where
+  mp h := or_iff_not_imp_left.mpr fun hp ↦ mul_left_cancel₀ hp (h.trans (mul_one p).symm)
+  mpr h := h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one
+
+end CancelMonoidWithZero
+end IsIdempotentElem
diff --git a/Mathlib/Algebra/GroupWithZero/Submonoid.lean b/Mathlib/Algebra/GroupWithZero/Submonoid.lean
new file mode 100644
index 00000000000000..4c8f758858a7e2
--- /dev/null
+++ b/Mathlib/Algebra/GroupWithZero/Submonoid.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.GroupWithZero.Divisibility
+
+/-!
+# Submonoid of primal elements
+-/
+
+/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
+def Submonoid.isPrimal (M₀ : Type*) [CancelCommMonoidWithZero M₀] : Submonoid M₀ where
+  carrier := {a | IsPrimal a}
+  mul_mem' := .mul
+  one_mem' := isUnit_one.isPrimal
diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean
new file mode 100644
index 00000000000000..0beb0f9e10ef25
--- /dev/null
+++ b/Mathlib/Algebra/Ring/Idempotent.lean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.GroupWithZero.Idempotent
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.Order.Notation
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.one_sub_iff`: In a (non-associative) ring, `a` is an idempotent if and only if
+  `1-a` is an idempotent.
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `a ^ (n+1) = a` for `a` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+variable {R : Type*}
+
+namespace IsIdempotentElem
+section NonAssocRing
+variable [NonAssocRing R] {a : R}
+
+lemma one_sub (h : IsIdempotentElem a) : IsIdempotentElem (1 - a) := by
+  rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
+
+@[simp]
+lemma one_sub_iff : IsIdempotentElem (1 - a) ↔ IsIdempotentElem a :=
+  ⟨fun h => sub_sub_cancel 1 a ▸ h.one_sub, IsIdempotentElem.one_sub⟩
+
+@[simp]
+lemma mul_one_sub_self (h : IsIdempotentElem a) : a * (1 - a) = 0 := by
+  rw [mul_sub, mul_one, h.eq, sub_self]
+
+@[simp]
+lemma one_sub_mul_self (h : IsIdempotentElem a) : (1 - a) * a = 0 := by
+  rw [sub_mul, one_mul, h.eq, sub_self]
+
+instance : HasCompl {a : R // IsIdempotentElem a} where compl a := ⟨1 - a, a.prop.one_sub⟩
+
+@[simp] lemma coe_compl (a : {a : R // IsIdempotentElem a}) : ↑aᶜ = (1 : R) - ↑a := rfl
+
+@[simp] lemma compl_compl (a : {a : R // IsIdempotentElem a}) : aᶜᶜ = a := by ext; simp
+@[simp] lemma zero_compl : (0 : {a : R // IsIdempotentElem a})ᶜ = 1 := by ext; simp
+@[simp] lemma one_compl : (1 : {a : R // IsIdempotentElem a})ᶜ = 0 := by ext; simp
+
+end NonAssocRing
+
+section Semiring
+variable [Semiring R] {a b : R}
+
+lemma of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b := by
+  simp_rw [IsIdempotentElem]; constructor
+  · conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
+  · conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]
+
+end Semiring
+
+section Ring
+variable [Ring R] {a b : R}
+
+lemma add_sub_mul_of_commute (h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
+    IsIdempotentElem (a + b - a * b) := by
+  convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1
+  · simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm]
+  · simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq]
+
+end Ring
+
+section CommRing
+variable [CommRing R] {a b : R}
+
+lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
+    IsIdempotentElem (a + b - a * b) := add_sub_mul_of_commute (.all ..) hp hq
+
+end CommRing
+end IsIdempotentElem
diff --git a/Mathlib/Algebra/Ring/Idempotents.lean b/Mathlib/Algebra/Ring/Idempotents.lean
deleted file mode 100644
index 9be312f90d4dad..00000000000000
--- a/Mathlib/Algebra/Ring/Idempotents.lean
+++ /dev/null
@@ -1,158 +0,0 @@
-/-
-Copyright (c) 2022 Christopher Hoskin. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christopher Hoskin
--/
-import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Commute.Defs
-import Mathlib.Algebra.Group.Hom.Defs
-import Mathlib.Algebra.Ring.Defs
-import Mathlib.Data.Subtype
-import Mathlib.Order.Notation
-
-/-!
-# Idempotents
-
-This file defines idempotents for an arbitrary multiplication and proves some basic results,
-including:
-
-* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
-  an idempotent;
-* `IsIdempotentElem.one_sub_iff`: In a (non-associative) ring, `p` is an idempotent if and only if
-  `1-p` is an idempotent.
-* `IsIdempotentElem.pow_succ_eq`: In a monoid `p ^ (n+1) = p` for `p` an idempotent and `n` a
-  natural number.
-
-## Tags
-
-projection, idempotent
--/
-
-
-variable {M N S M₀ M₁ R G G₀ : Type*}
-variable [Mul M] [Monoid N] [Semigroup S] [MulZeroClass M₀] [MulOneClass M₁] [NonAssocRing R]
-  [Group G] [CancelMonoidWithZero G₀]
-
-/-- An element `p` is said to be idempotent if `p * p = p`
--/
-def IsIdempotentElem (p : M) : Prop :=
-  p * p = p
-
-namespace IsIdempotentElem
-
-theorem of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
-  Std.IdempotentOp.idempotent a
-
-theorem eq {p : M} (h : IsIdempotentElem p) : p * p = p :=
-  h
-
-theorem mul_of_commute {p q : S} (h : Commute p q) (h₁ : IsIdempotentElem p)
-    (h₂ : IsIdempotentElem q) : IsIdempotentElem (p * q) := by
-  rw [IsIdempotentElem, mul_assoc, ← mul_assoc q, ← h.eq, mul_assoc p, h₂.eq, ← mul_assoc, h₁.eq]
-
-lemma mul {M} [CommSemigroup M] {e₁ e₂ : M}
-    (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) : IsIdempotentElem (e₁ * e₂) :=
-  he₁.mul_of_commute (.all e₁ e₂) he₂
-
-theorem zero : IsIdempotentElem (0 : M₀) :=
-  mul_zero _
-
-theorem one : IsIdempotentElem (1 : M₁) :=
-  mul_one _
-
-theorem one_sub {p : R} (h : IsIdempotentElem p) : IsIdempotentElem (1 - p) := by
-  rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-
-@[simp]
-theorem one_sub_iff {p : R} : IsIdempotentElem (1 - p) ↔ IsIdempotentElem p :=
-  ⟨fun h => sub_sub_cancel 1 p ▸ h.one_sub, IsIdempotentElem.one_sub⟩
-
-@[simp]
-theorem mul_one_sub_self {p : R} (h : IsIdempotentElem p) : p * (1 - p) = 0 := by
-  rw [mul_sub, mul_one, h.eq, sub_self]
-
-@[simp]
-theorem one_sub_mul_self {p : R} (h : IsIdempotentElem p) : (1 - p) * p = 0 := by
-  rw [sub_mul, one_mul, h.eq, sub_self]
-
-theorem add_sub_mul_of_commute {R} [Ring R] {p q : R} (h : Commute p q)
-    (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
-    IsIdempotentElem (p + q - p * q) := by
-  convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1
-  · simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm]
-  · simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq]
-
-theorem add_sub_mul {R} [CommRing R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
-    IsIdempotentElem (p + q - p * q) :=
-  add_sub_mul_of_commute (mul_comm p q) hp hq
-
-theorem pow {p : N} (n : ℕ) (h : IsIdempotentElem p) : IsIdempotentElem (p ^ n) :=
-  Nat.recOn n ((pow_zero p).symm ▸ one) fun n _ =>
-    show p ^ n.succ * p ^ n.succ = p ^ n.succ by
-      conv_rhs => rw [← h.eq] -- Porting note: was `nth_rw 3 [← h.eq]`
-      rw [← sq, ← sq, ← pow_mul, ← pow_mul']
-
-theorem pow_succ_eq {p : N} (n : ℕ) (h : IsIdempotentElem p) : p ^ (n + 1) = p :=
-  Nat.recOn n ((Nat.zero_add 1).symm ▸ pow_one p) fun n ih => by rw [pow_succ, ih, h.eq]
-
-@[simp]
-theorem iff_eq_one {p : G} : IsIdempotentElem p ↔ p = 1 :=
-  Iff.intro (fun h => mul_left_cancel ((mul_one p).symm ▸ h.eq : p * p = p * 1)) fun h =>
-    h.symm ▸ one
-
-@[simp]
-theorem iff_eq_zero_or_one {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1 := by
-  refine
-    Iff.intro (fun h => or_iff_not_imp_left.mpr fun hp => ?_) fun h =>
-      h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one
-  exact mul_left_cancel₀ hp (h.trans (mul_one p).symm)
-
-lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M}
-    (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e) := by
-  rw [IsIdempotentElem, ← map_mul, he.eq]
-
-lemma of_mul_add {R} [Semiring R] {e₁ e₂ : R} (mul : e₁ * e₂ = 0) (add : e₁ + e₂ = 1) :
-    IsIdempotentElem e₁ ∧ IsIdempotentElem e₂ := by
-  simp_rw [IsIdempotentElem]; constructor
-  · conv_rhs => rw [← mul_one e₁, ← add, mul_add, mul, add_zero]
-  · conv_rhs => rw [← one_mul e₂, ← add, add_mul, mul, zero_add]
-
-/-! ### Instances on `Subtype IsIdempotentElem` -/
-
-
-section Instances
-
-instance : Zero { p : M₀ // IsIdempotentElem p } where zero := ⟨0, zero⟩
-
-@[simp]
-theorem coe_zero : ↑(0 : { p : M₀ // IsIdempotentElem p }) = (0 : M₀) :=
-  rfl
-
-instance : One { p : M₁ // IsIdempotentElem p } where one := ⟨1, one⟩
-
-@[simp]
-theorem coe_one : ↑(1 : { p : M₁ // IsIdempotentElem p }) = (1 : M₁) :=
-  rfl
-
-instance : HasCompl { p : R // IsIdempotentElem p } :=
-  ⟨fun p => ⟨1 - p, p.prop.one_sub⟩⟩
-
-@[simp]
-theorem coe_compl (p : { p : R // IsIdempotentElem p }) : ↑pᶜ = (1 : R) - ↑p :=
-  rfl
-
-@[simp]
-theorem compl_compl (p : { p : R // IsIdempotentElem p }) : pᶜᶜ = p :=
-  Subtype.ext <| sub_sub_cancel _ _
-
-@[simp]
-theorem zero_compl : (0 : { p : R // IsIdempotentElem p })ᶜ = 1 :=
-  Subtype.ext <| sub_zero _
-
-@[simp]
-theorem one_compl : (1 : { p : R // IsIdempotentElem p })ᶜ = 0 :=
-  Subtype.ext <| sub_self _
-
-end Instances
-
-end IsIdempotentElem
diff --git a/Mathlib/Algebra/Ring/Submonoid.lean b/Mathlib/Algebra/Ring/Submonoid.lean
new file mode 100644
index 00000000000000..d07493ac6ce558
--- /dev/null
+++ b/Mathlib/Algebra/Ring/Submonoid.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
+Amelia Livingston, Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Submonoid.Basic
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.Tactic.MinImports
+
+/-! # Lemmas about additive closures of `Subsemigroup`. -/
+
+open AddSubmonoid
+
+namespace MulMemClass
+variable {M R : Type*} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M}
+  {a b : R}
+
+/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
+and an element of `M` is contained in the additive closure of `M`. -/
+lemma mul_right_mem_add_closure (ha : a ∈ closure (S : Set R)) (hb : b ∈ S) :
+    a * b ∈ closure (S : Set R) := by
+  induction ha using closure_induction with
+  | mem r hr => exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
+  | one => simp only [zero_mul, zero_mem _]
+  | mul r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
+
+/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
+additive closure of `M`. -/
+lemma mul_mem_add_closure (ha : a ∈ closure (S : Set R))
+    (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R) := by
+  induction hb using closure_induction with
+  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
+  | one => simp only [mul_zero, zero_mem _]
+  | mul r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
+
+/-- The product of an element of `S` and an element of the additive closure of a multiplicative
+submonoid `S` is contained in the additive closure of `S`. -/
+lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ closure (S : Set R)) :
+    a * b ∈ closure (S : Set R) :=
+  mul_mem_add_closure (AddSubmonoid.mem_closure.mpr fun _sT hT => hT ha) hb
+
+end MulMemClass
diff --git a/Mathlib/Analysis/NormedSpace/MStructure.lean b/Mathlib/Analysis/NormedSpace/MStructure.lean
index daa293a5f0d87d..94758ad5cf2918 100644
--- a/Mathlib/Analysis/NormedSpace/MStructure.lean
+++ b/Mathlib/Analysis/NormedSpace/MStructure.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Order.Basic
 import Mathlib.Tactic.NoncommRing
diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean
index 9da8fb60044f61..1956ea622b43af 100644
--- a/Mathlib/LinearAlgebra/Span/Basic.lean
+++ b/Mathlib/LinearAlgebra/Span/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Algebra.Module.Submodule.EqLocus
 import Mathlib.Algebra.Module.Submodule.Equiv
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.NoZeroSMulDivisors.Basic
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.LinearAlgebra.Span.Defs
 import Mathlib.Order.CompactlyGenerated.Basic
diff --git a/Mathlib/Order/Idempotents.lean b/Mathlib/Order/Idempotents.lean
index e872f7be5ab00c..fd3c4ab4bc208c 100644
--- a/Mathlib/Order/Idempotents.lean
+++ b/Mathlib/Order/Idempotents.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025 Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Order.BooleanAlgebra
 import Mathlib.Order.Hom.Basic
 
diff --git a/Mathlib/RingTheory/Filtration.lean b/Mathlib/RingTheory/Filtration.lean
index ea599e07132839..e7e62f2646f480 100644
--- a/Mathlib/RingTheory/Filtration.lean
+++ b/Mathlib/RingTheory/Filtration.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Polynomial.Module.Basic
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Order.Basic
 import Mathlib.Order.Hom.Lattice
 import Mathlib.RingTheory.Finiteness.Nakayama
diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean
index 727ba571e6518f..611a2eabec2f72 100644
--- a/Mathlib/RingTheory/Ideal/Cotangent.lean
+++ b/Mathlib/RingTheory/Ideal/Cotangent.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Algebra.Module.Torsion
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
diff --git a/Mathlib/RingTheory/Ideal/IdempotentFG.lean b/Mathlib/RingTheory/Ideal/IdempotentFG.lean
index caeb5aba8980b2..707f70ab3dad0a 100644
--- a/Mathlib/RingTheory/Ideal/IdempotentFG.lean
+++ b/Mathlib/RingTheory/Ideal/IdempotentFG.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro, Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Buzzard
 -/
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Order.Basic
 import Mathlib.RingTheory.Finiteness.Nakayama
 
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
index 45d4fd35b00b3f..3c64ca5b8140a0 100644
--- a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
+++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Associated.Basic
 import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.Group.Submonoid.BigOperators
+import Mathlib.Algebra.GroupWithZero.Submonoid
 import Mathlib.Order.WellFounded
 
 /-!