feat: non-zero smul-divisors (#7138)

If $R$ is a monoid with $0$ and $M$ an additive monoid with an $R$-action, then the set of non-zero smul-divisors of $R$ is a submonoid. for any $r \in R$, $r$ is a non-zero smul-divisors if and only if for any $m\in M$, $r \cdot m = 0$ implies $m = 0$. These elements are also called $M$-regular. They are useful in regular sequences.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/RingTheory/NonZeroDivisors.lean

@@ -5,26 +5,29 @@ Authors: Kenny Lau, Devon Tuma
 -/
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Membership
+import Mathlib.GroupTheory.Subgroup.MulOpposite
 
 #align_import ring_theory.non_zero_divisors from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 
 /-!
-# Non-zero divisors
+# Non-zero divisors and smul-divisors
 
-In this file we define the submonoid `nonZeroDivisors` of a `MonoidWithZero`.
+In this file we define the submonoid `nonZeroDivisors` and `nonZeroSMulDivisors` of a
+`MonoidWithZero`.
 
 ## Notations
 
-This file declares the notation `R⁰` for the submonoid of non-zero-divisors of `R`,
-in the locale `nonZeroDivisors`.
+This file declares the notations:
+- `R⁰` for the submonoid of non-zero-divisors of `R`, in the locale `nonZeroDivisors`.
+- `R⁰[M]` for the submonoid of non-zero smul-divisors of `R` with respect to `M`, in the locale
+  `nonZeroSMulDivisors`
 
-Use the statement `open nonZeroDivisors` to access this notation in your own code.
+Use the statement `open scoped nonZeroDivisors nonZeroSMulDivisors` to access this notation in
+your own code.
 
 -/
 
 
-section nonZeroDivisors
-
 /-- The submonoid of non-zero-divisors of a `MonoidWithZero` `R`. -/
 def nonZeroDivisors (R : Type*) [MonoidWithZero R] : Submonoid R where
   carrier := { x | ∀ z, z * x = 0 → z = 0 }
@@ -37,6 +40,19 @@ def nonZeroDivisors (R : Type*) [MonoidWithZero R] : Submonoid R where
 /-- The notation for the submonoid of non-zerodivisors. -/
 scoped[nonZeroDivisors] notation:9000 R "⁰" => nonZeroDivisors R
 
+/-- Let `R` be a monoid with zero and `M` an additive monoid with an `R`-action, then the collection
+of non-zero smul-divisors forms a submonoid. These elements are also called `M`-regular.-/
+def nonZeroSMulDivisors (R : Type*) [MonoidWithZero R] (M : Type _) [Zero M] [MulAction R M] :
+    Submonoid R where
+  carrier := { r | ∀ m : M, r • m = 0 → m = 0}
+  one_mem' m h := (one_smul R m) ▸ h
+  mul_mem' {r₁ r₂} h₁ h₂ m H := h₂ _ <| h₁ _ <| mul_smul r₁ r₂ m ▸ H
+
+/-- The notation for the submonoid of non-zero smul-divisors. -/
+scoped[nonZeroSMulDivisors] notation:9000 R "⁰[" M "]" => nonZeroSMulDivisors R M
+
+section nonZeroDivisors
+
 open nonZeroDivisors
 
 variable {M M' M₁ R R' F : Type*} [MonoidWithZero M] [MonoidWithZero M'] [CommMonoidWithZero M₁]
@@ -178,3 +194,25 @@ theorem prod_zero_iff_exists_zero [NoZeroDivisors M₁] [Nontrivial M₁] {s : M
 #align prod_zero_iff_exists_zero prod_zero_iff_exists_zero
 
 end nonZeroDivisors
+
+section nonZeroSMulDivisors
+
+open nonZeroSMulDivisors nonZeroDivisors
+
+variable {R M : Type*} [MonoidWithZero R] [Zero M] [MulAction R M]
+
+lemma mem_nonZeroSMulDivisors_iff {x : R} : x ∈ R⁰[M] ↔ ∀ (m : M), x • m = 0 → m = 0 := Iff.rfl
+
+variable (R)
+
+@[simp]
+lemma unop_nonZeroSmulDivisors_mulOpposite_eq_nonZeroDivisors :
+    (Rᵐᵒᵖ ⁰[R]).unop = R⁰ := rfl
+
+/-- The non-zero `•`-divisors with `•` as right multiplication correspond with the non-zero
+divisors. Note that the `MulOpposite` is needed because we defined `nonZeroDivisors` with
+multiplication on the right. -/
+lemma nonZeroSmulDivisors_mulOpposite_eq_op_nonZeroDivisors :
+    Rᵐᵒᵖ ⁰[R] = R⁰.op := rfl
+
+end nonZeroSMulDivisors