chore: Move RingTheory/NonZeroDivisors under Algebra instead. (#8685

)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -217,6 +217,7 @@ import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.NeZero
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.GroupWithZero.Power
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Units.Basic
@@ -2210,7 +2211,6 @@ import Mathlib.GroupTheory.Submonoid.Membership
 import Mathlib.GroupTheory.Submonoid.MulOpposite
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Pointwise
-import Mathlib.GroupTheory.Submonoid.ZeroDivisors
 import Mathlib.GroupTheory.Subsemigroup.Basic
 import Mathlib.GroupTheory.Subsemigroup.Center
 import Mathlib.GroupTheory.Subsemigroup.Centralizer
@@ -3068,7 +3068,6 @@ import Mathlib.RingTheory.Nilpotent
 import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.NonUnitalSubring.Basic
 import Mathlib.RingTheory.NonUnitalSubsemiring.Basic
-import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.Norm
 import Mathlib.RingTheory.Nullstellensatz
 import Mathlib.RingTheory.OreLocalization.Basic

Mathlib/RingTheory/NonZeroDivisors.lean → Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau, Devon Tuma
+Authors: Kenny Lau, Devon Tuma, Oliver Nash
 -/
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Membership
@@ -13,7 +13,8 @@ import Mathlib.GroupTheory.Subgroup.MulOpposite
 # Non-zero divisors and smul-divisors
 
 In this file we define the submonoid `nonZeroDivisors` and `nonZeroSMulDivisors` of a
-`MonoidWithZero`.
+`MonoidWithZero`. We also define `nonZeroDivisorsLeft` and `nonZeroDivisorsRight` for
+non-commutative monoids.
 
 ## Notations
 
@@ -27,6 +28,50 @@ your own code.
 
 -/
 
+variable (M₀ : Type*) [MonoidWithZero M₀]
+
+/-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
+`Submonoid`. -/
+def nonZeroDivisorsLeft : Submonoid M₀ where
+  carrier := {x | ∀ y, y * x = 0 → y = 0}
+  one_mem' := by simp
+  mul_mem' {x} {y} hx hy := fun z hz ↦ hx _ <| hy _ (mul_assoc z x y ▸ hz)
+
+@[simp] lemma mem_nonZeroDivisorsLeft_iff {x : M₀} :
+    x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0 :=
+  Iff.rfl
+
+/-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
+`Submonoid`. -/
+def nonZeroDivisorsRight : Submonoid M₀ where
+  carrier := {x | ∀ y, x * y = 0 → y = 0}
+  one_mem' := by simp
+  mul_mem' := fun {x} {y} hx hy z hz ↦ hy _ (hx _ ((mul_assoc x y z).symm ▸ hz))
+
+@[simp] lemma mem_nonZeroDivisorsRight_iff {x : M₀} :
+    x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0 :=
+  Iff.rfl
+
+lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
+    nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by
+  ext x; simp [mul_comm x]
+
+@[simp] lemma coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
+    nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0} := by
+  ext x
+  simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and,
+    Set.mem_setOf_eq]
+  refine' ⟨fun h ↦ _, fun hx y hx' ↦ by contradiction⟩
+  contrapose! h
+  exact ⟨1, h, one_ne_zero⟩
+
+@[simp] lemma coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
+    nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0} := by
+  ext x
+  simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
+  refine' ⟨fun h ↦ _, fun hx y hx' ↦ by aesop⟩
+  contrapose! h
+  exact ⟨1, Or.inl h, one_ne_zero⟩
 
 /-- The submonoid of non-zero-divisors of a `MonoidWithZero` `R`. -/
 def nonZeroDivisors (R : Type*) [MonoidWithZero R] : Submonoid R where

Mathlib/LinearAlgebra/SesquilinearForm.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Module.LinearMap
 import Mathlib.LinearAlgebra.Basis.Bilinear
 import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.Algebra.EuclideanDomain.Instances
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 
 #align_import linear_algebra.sesquilinear_form from "leanprover-community/mathlib"@"87c54600fe3cdc7d32ff5b50873ac724d86aef8d"
 

Mathlib/RingTheory/Ideal/Operations.lean

@@ -9,7 +9,7 @@ import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.LinearAlgebra.Basis.Bilinear
 import Mathlib.RingTheory.Coprime.Lemmas
 import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 
 #align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"
 

Mathlib/RingTheory/Localization/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.GroupTheory.MonoidLocalization
 import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Tactic.Ring
 
 #align_import ring_theory.localization.basic from "leanprover-community/mathlib"@"b69c9a770ecf37eb21f7b8cf4fa00de3b62694ec"

Mathlib/RingTheory/Localization/Integral.lean

@@ -10,7 +10,7 @@ import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.RingTheory.IntegralClosure
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Localization.Integer
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 
 #align_import ring_theory.localization.integral from "leanprover-community/mathlib"@"831c494092374cfe9f50591ed0ac81a25efc5b86"
 

Mathlib/RingTheory/Nilpotent.lean

@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Algebra.Algebra.Bilinear
-import Mathlib.GroupTheory.Submonoid.ZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Algebra.GeomSum
 import Mathlib.LinearAlgebra.Matrix.ToLin

Mathlib/RingTheory/OreLocalization/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer, Kevin Klinge
 -/
 import Mathlib.GroupTheory.MonoidLocalization
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.OreSet
 import Mathlib.Tactic.NoncommRing
 

Mathlib/RingTheory/Polynomial/ScaleRoots.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Devon Tuma
 -/
-import Mathlib.RingTheory.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Data.Polynomial.AlgebraMap
 
 #align_import ring_theory.polynomial.scale_roots from "leanprover-community/mathlib"@"40ac1b258344e0c2b4568dc37bfad937ec35a727"