chore(Submonoid/Membership): don't import MonoidWithZero

See #10327 for the new copyright header

Mathlib.lean

@@ -409,6 +409,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
@@ -945,6 +946,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

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -9,10 +9,7 @@ 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.Int.Defs
 import Mathlib.Data.Fintype.Card
-import Mathlib.Data.Nat.Cast.Basic
 
 /-!
 # Submonoids: membership criteria
@@ -33,8 +30,7 @@ In this file we prove various facts about membership in a submonoid:
 submonoid, submonoids
 -/
 
--- We don't need ordered structures to establish basic membership facts for submonoids
-assert_not_exists OrderedSemiring
+assert_not_exists MonoidWithZero
 
 variable {M A B : Type*}
 
@@ -334,7 +330,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 +479,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 +514,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

Mathlib/Algebra/Group/Submonoid/Pointwise.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Order.BigOperators.Group.List
+import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Order.WellFoundedSet
 

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.GroupWithZero.Associated
 import Mathlib.Algebra.GroupWithZero.Opposite
+import Mathlib.Algebra.Ring.Defs
 
 /-!
 # Non-zero divisors and smul-divisors

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.Defs
+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

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

Mathlib/GroupTheory/MonoidLocalization/Away.lean

@@ -17,6 +17,8 @@ localization, monoid localization, quotient monoid, congruence relation, charact
 commutative monoid, grothendieck group
 -/
 
+assert_not_exists MonoidWithZero
+
 open Function
 
 section CommMonoid

Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -11,6 +11,7 @@ import Mathlib.Algebra.GroupWithZero.Center
 import Mathlib.Algebra.Ring.Center
 import Mathlib.Algebra.Ring.Centralizer
 import Mathlib.Algebra.Ring.Prod
+import Mathlib.Algebra.Ring.Submonoid
 import Mathlib.Data.Set.Finite.Range
 import Mathlib.GroupTheory.Subsemigroup.Centralizer
 import Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker, Aaron Anderson
 -/
 import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
-import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.Group.Submonoid.BigOperators
 import Mathlib.Algebra.GroupWithZero.Associated
+import Mathlib.Algebra.GroupWithZero.Submonoid
 import Mathlib.Order.WellFounded
 
 /-!