chore(NonZeroDivisors): clean up (#21288)

Follow-up to #20871, which was only code moves.

Author: YaelDillies

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -18,8 +18,8 @@ non-commutative monoids.
 ## Notations
 
 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
+- `M₀⁰` for the submonoid of non-zero-divisors of `M₀`, in the locale `nonZeroDivisors`.
+- `M₀⁰[M]` for the submonoid of non-zero smul-divisors of `M₀` with respect to `M`, in the locale
   `nonZeroSMulDivisors`
 
 Use the statement `open scoped nonZeroDivisors nonZeroSMulDivisors` to access this notation in
@@ -29,8 +29,10 @@ your own code.
 
 assert_not_exists Ring
 
+open Function
+
 section
-variable (M₀ : Type*) [MonoidWithZero M₀]
+variable (M₀ : Type*) [MonoidWithZero M₀] {x : M₀}
 
 /-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
 `Submonoid`. -/
@@ -39,12 +41,11 @@ def nonZeroDivisorsLeft : Submonoid M₀ where
   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
+@[simp]
+lemma mem_nonZeroDivisorsLeft_iff : x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0 := .rfl
 
-lemma nmem_nonZeroDivisorsLeft_iff {r : M₀} :
-    r ∉ nonZeroDivisorsLeft M₀ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty := by
+lemma nmem_nonZeroDivisorsLeft_iff :
+    x ∉ nonZeroDivisorsLeft M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty := by
   simpa [mem_nonZeroDivisorsLeft_iff] using Set.nonempty_def.symm
 
 /-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
@@ -54,12 +55,11 @@ def nonZeroDivisorsRight : Submonoid M₀ where
   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
+@[simp]
+lemma mem_nonZeroDivisorsRight_iff : x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0 := .rfl
 
-lemma nmem_nonZeroDivisorsRight_iff {r : M₀} :
-    r ∉ nonZeroDivisorsRight M₀ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty := by
+lemma nmem_nonZeroDivisorsRight_iff :
+    x ∉ nonZeroDivisorsRight M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty := by
   simpa [mem_nonZeroDivisorsRight_iff] using Set.nonempty_def.symm
 
 lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
@@ -85,148 +85,160 @@ lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
 
 end
 
-/-- The submonoid of non-zero-divisors of a `MonoidWithZero` `R`. -/
-def nonZeroDivisors (R : Type*) [MonoidWithZero R] : Submonoid R where
+/-- The submonoid of non-zero-divisors of a `MonoidWithZero` `M₀`. -/
+def nonZeroDivisors (M₀ : Type*) [MonoidWithZero M₀] : Submonoid M₀ where
   carrier := { x | ∀ z, z * x = 0 → z = 0 }
   one_mem' _ hz := by rwa [mul_one] at hz
   mul_mem' hx₁ hx₂ _ hz := by
     rw [← mul_assoc] at hz
     exact hx₁ _ (hx₂ _ hz)
 
-/-- The notation for the submonoid of non-zerodivisors. -/
-scoped[nonZeroDivisors] notation:9000 R "⁰" => nonZeroDivisors R
+/-- The notation for the submonoid of non-zero divisors. -/
+scoped[nonZeroDivisors] notation:9000 M₀ "⁰" => nonZeroDivisors M₀
 
-/-- 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
+/-- Let `M₀` be a monoid with zero and `M` an additive monoid with an `M₀`-action, then the
+collection of non-zero smul-divisors forms a submonoid.
+
+These elements are also called `M`-regular. -/
+def nonZeroSMulDivisors (M₀ : Type*) [MonoidWithZero M₀] (M : Type*) [Zero M] [MulAction M₀ M] :
+    Submonoid M₀ where
   carrier := { r | ∀ m : M, r • m = 0 → m = 0}
-  one_mem' m h := (one_smul R m) ▸ h
+  one_mem' m h := (one_smul M₀ 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
+scoped[nonZeroSMulDivisors] notation:9000 M₀ "⁰[" M "]" => nonZeroSMulDivisors M₀ M
 
 open nonZeroDivisors
 
 section MonoidWithZero
-variable {M M' M₁ R R' F : Type*} [MonoidWithZero M] [MonoidWithZero M'] [CommMonoidWithZero M₁]
+variable {F M₀ M₀' : Type*} [MonoidWithZero M₀] [MonoidWithZero M₀'] {r x y : M₀}
 
-theorem mem_nonZeroDivisors_iff {r : M} : r ∈ M⁰ ↔ ∀ x, x * r = 0 → x = 0 := Iff.rfl
+theorem mem_nonZeroDivisors_iff : r ∈ M₀⁰ ↔ ∀ x, x * r = 0 → x = 0 := Iff.rfl
 
-lemma nmem_nonZeroDivisors_iff {r : M} : r ∉ M⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty := by
+lemma nmem_nonZeroDivisors_iff : r ∉ M₀⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty := by
   simpa [mem_nonZeroDivisors_iff] using Set.nonempty_def.symm
 
-theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {x r : M} (hr : r ∈ M⁰) : x * r = 0 ↔ x = 0 :=
+theorem mul_right_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : x * r = 0 ↔ x = 0 :=
   ⟨hr _, by simp +contextual⟩
+
 @[simp]
-theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {x : M} {c : M⁰} : x * c = 0 ↔ x = 0 :=
+theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {c : M₀⁰} : x * c = 0 ↔ x = 0 :=
   mul_right_mem_nonZeroDivisors_eq_zero_iff c.prop
 
-theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {r x : M₁} (hr : r ∈ M₁⁰) : r * x = 0 ↔ x = 0 := by
-  rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
+lemma IsUnit.mem_nonZeroDivisors (hx : IsUnit x) : x ∈ M₀⁰ := fun _ ↦ hx.mul_left_eq_zero.mp
 
-@[simp]
-theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {c : M₁⁰} {x : M₁} : (c : M₁) * x = 0 ↔ x = 0 :=
-  mul_left_mem_nonZeroDivisors_eq_zero_iff c.prop
+section Nontrivial
+variable [Nontrivial M₀]
 
-theorem zero_not_mem_nonZeroDivisors [Nontrivial M] : 0 ∉ M⁰ :=
-  fun h ↦ one_ne_zero <| h 1 <| mul_zero _
+theorem zero_not_mem_nonZeroDivisors : 0 ∉ M₀⁰ := fun h ↦ one_ne_zero <| h 1 <| mul_zero _
 
-theorem nonZeroDivisors.ne_zero [Nontrivial M] {x} (hx : x ∈ M⁰) : x ≠ 0 :=
+theorem nonZeroDivisors.ne_zero (hx : x ∈ M₀⁰) : x ≠ 0 :=
   ne_of_mem_of_not_mem hx zero_not_mem_nonZeroDivisors
 
 @[simp]
-theorem nonZeroDivisors.coe_ne_zero [Nontrivial M] (x : M⁰) : (x : M) ≠ 0 :=
-  nonZeroDivisors.ne_zero x.2
+theorem nonZeroDivisors.coe_ne_zero (x : M₀⁰) : (x : M₀) ≠ 0 := nonZeroDivisors.ne_zero x.2
 
-theorem mul_mem_nonZeroDivisors {a b : M₁} : a * b ∈ M₁⁰ ↔ a ∈ M₁⁰ ∧ b ∈ M₁⁰ := by
-  constructor
-  · intro h
-    constructor <;> intro x h' <;> apply h
-    · rw [← mul_assoc, h', zero_mul]
-    · rw [mul_comm a b, ← mul_assoc, h', zero_mul]
-  · rintro ⟨ha, hb⟩ x hx
-    apply ha
-    apply hb
-    rw [mul_assoc, hx]
+end Nontrivial
 
-lemma IsUnit.mem_nonZeroDivisors {a : M} (ha : IsUnit a) : a ∈ M⁰ :=
-  fun _ h ↦ ha.mul_left_eq_zero.mp h
+section NoZeroDivisors
+variable [NoZeroDivisors M₀]
 
-theorem eq_zero_of_ne_zero_of_mul_right_eq_zero [NoZeroDivisors M] {x y : M} (hnx : x ≠ 0)
-    (hxy : y * x = 0) : y = 0 :=
-  Or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
+theorem eq_zero_of_ne_zero_of_mul_right_eq_zero (hx : x ≠ 0) (hxy : y * x = 0) : y = 0 :=
+  Or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hx
 
-theorem eq_zero_of_ne_zero_of_mul_left_eq_zero [NoZeroDivisors M] {x y : M} (hnx : x ≠ 0)
-    (hxy : x * y = 0) : y = 0 :=
-  Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
+theorem eq_zero_of_ne_zero_of_mul_left_eq_zero (hx : x ≠ 0) (hxy : x * y = 0) : y = 0 :=
+  Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hx
 
-theorem mem_nonZeroDivisors_of_ne_zero [NoZeroDivisors M] {x : M} (hx : x ≠ 0) : x ∈ M⁰ := fun _ ↦
+theorem mem_nonZeroDivisors_of_ne_zero (hx : x ≠ 0) : x ∈ M₀⁰ := fun _ ↦
   eq_zero_of_ne_zero_of_mul_right_eq_zero hx
 
-@[simp] lemma mem_nonZeroDivisors_iff_ne_zero [NoZeroDivisors M] [Nontrivial M] {x : M} :
-    x ∈ M⁰ ↔ x ≠ 0 := ⟨nonZeroDivisors.ne_zero, mem_nonZeroDivisors_of_ne_zero⟩
+@[simp] lemma mem_nonZeroDivisors_iff_ne_zero [Nontrivial M₀] : x ∈ M₀⁰ ↔ x ≠ 0 :=
+  ⟨nonZeroDivisors.ne_zero, mem_nonZeroDivisors_of_ne_zero⟩
+
+theorem le_nonZeroDivisors_of_noZeroDivisors {S : Submonoid M₀} (hS : (0 : M₀) ∉ S) :
+    S ≤ M₀⁰ := fun _ hx _ hy ↦
+  Or.recOn (eq_zero_or_eq_zero_of_mul_eq_zero hy) id fun h ↦
+    absurd (h ▸ hx : (0 : M₀) ∈ S) hS
+
+theorem powers_le_nonZeroDivisors_of_noZeroDivisors (hx : x ≠ 0) : Submonoid.powers x ≤ M₀⁰ :=
+  le_nonZeroDivisors_of_noZeroDivisors fun h ↦ hx (h.recOn fun _ ↦ pow_eq_zero)
+
+end NoZeroDivisors
 
-variable [FunLike F M M']
+variable [FunLike F M₀ M₀']
 
-theorem map_ne_zero_of_mem_nonZeroDivisors [Nontrivial M] [ZeroHomClass F M M'] (g : F)
-    (hg : Function.Injective (g : M → M')) {x : M} (h : x ∈ M⁰) : g x ≠ 0 := fun h0 ↦
+theorem map_ne_zero_of_mem_nonZeroDivisors [Nontrivial M₀] [ZeroHomClass F M₀ M₀'] (g : F)
+    (hg : Injective (g : M₀ → M₀')) {x : M₀} (h : x ∈ M₀⁰) : g x ≠ 0 := fun h0 ↦
   one_ne_zero (h 1 ((one_mul x).symm ▸ hg (h0.trans (map_zero g).symm)))
 
-theorem map_mem_nonZeroDivisors [Nontrivial M] [NoZeroDivisors M'] [ZeroHomClass F M M'] (g : F)
-    (hg : Function.Injective g) {x : M} (h : x ∈ M⁰) : g x ∈ M'⁰ := fun _ hz ↦
+theorem map_mem_nonZeroDivisors [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F)
+    (hg : Injective g) {x : M₀} (h : x ∈ M₀⁰) : g x ∈ M₀'⁰ := fun _ hz ↦
   eq_zero_of_ne_zero_of_mul_right_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h) hz
 
-theorem MulEquivClass.map_nonZeroDivisors {R S F : Type*} [MonoidWithZero R] [MonoidWithZero S]
-    [EquivLike F R S] [MulEquivClass F R S] (h : F) :
-    Submonoid.map h (nonZeroDivisors R) = nonZeroDivisors S := by
-  let h : R ≃* S := h
+theorem MulEquivClass.map_nonZeroDivisors {M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S]
+    [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) :
+    Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S := by
+  let h : M₀ ≃* S := h
   show Submonoid.map h.toMonoidHom _ = _
   ext
   simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
     ← h.symm.forall_congr_right, h.symm.coe_toMonoidHom, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv,
     ← map_mul, map_eq_zero_iff _ h.symm.injective]
 
-theorem le_nonZeroDivisors_of_noZeroDivisors [NoZeroDivisors M] {S : Submonoid M}
-    (hS : (0 : M) ∉ S) : S ≤ M⁰ := fun _ hx _ hy ↦
-  Or.recOn (eq_zero_or_eq_zero_of_mul_eq_zero hy) id fun h ↦
-    absurd (h ▸ hx : (0 : M) ∈ S) hS
-
-theorem powers_le_nonZeroDivisors_of_noZeroDivisors [NoZeroDivisors M] {a : M} (ha : a ≠ 0) :
-    Submonoid.powers a ≤ M⁰ :=
-  le_nonZeroDivisors_of_noZeroDivisors fun h ↦ absurd (h.recOn fun _ hn ↦ pow_eq_zero hn) ha
-
-theorem map_le_nonZeroDivisors_of_injective [NoZeroDivisors M'] [MonoidWithZeroHomClass F M M']
-    (f : F) (hf : Function.Injective f) {S : Submonoid M} (hS : S ≤ M⁰) : S.map f ≤ M'⁰ := by
-  cases subsingleton_or_nontrivial M
+theorem map_le_nonZeroDivisors_of_injective [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀']
+    (f : F) (hf : Injective f) {S : Submonoid M₀} (hS : S ≤ M₀⁰) : S.map f ≤ M₀'⁰ := by
+  cases subsingleton_or_nontrivial M₀
   · simp [Subsingleton.elim S ⊥]
-  · exact le_nonZeroDivisors_of_noZeroDivisors fun h ↦
-      let ⟨x, hx, hx0⟩ := h
-      zero_ne_one (hS (hf (hx0.trans (map_zero f).symm) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm
+  · refine le_nonZeroDivisors_of_noZeroDivisors ?_
+    rintro ⟨x, hx, hx0⟩
+    exact one_ne_zero <| hS (hf (hx0.trans (map_zero f).symm) ▸ hx : 0 ∈ S) 1 (mul_zero 1)
 
-theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M']
-    [MonoidWithZeroHomClass F M M'] (f : F) (hf : Function.Injective f) : M⁰ ≤ M'⁰.comap f :=
+theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M₀']
+    [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Injective f) : M₀⁰ ≤ M₀'⁰.comap f :=
   Submonoid.le_comap_of_map_le _ (map_le_nonZeroDivisors_of_injective _ hf le_rfl)
 
 /-- If an element maps to a non-zero-divisor via injective homomorphism,
-then it is non-zero-divisor. -/
-theorem mem_nonZeroDivisors_of_injective [MonoidWithZeroHomClass F M M'] {f : F}
-    (hf : Function.Injective f) {a : M} (ha : f a ∈ M'⁰) : a ∈ M⁰ :=
-  fun x hx ↦ hf <| map_zero f ▸ ha (f x) (map_mul f x a ▸ map_zero f ▸ congrArg f hx)
+then it is a non-zero-divisor. -/
+theorem mem_nonZeroDivisors_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F}
+    (hf : Injective f) (hx : f x ∈ M₀'⁰) : x ∈ M₀⁰ :=
+  fun y hy ↦ hf <| map_zero f ▸ hx (f y) (map_mul f y x ▸ map_zero f ▸ congrArg f hy)
 
 @[deprecated (since := "2025-02-03")]
 alias mem_nonZeroDivisor_of_injective := mem_nonZeroDivisors_of_injective
 
-theorem comap_nonZeroDivisors_le_of_injective [MonoidWithZeroHomClass F M M'] {f : F}
-    (hf : Function.Injective f) : M'⁰.comap f ≤ M⁰ :=
+theorem comap_nonZeroDivisors_le_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F}
+    (hf : Injective f) : M₀'⁰.comap f ≤ M₀⁰ :=
   fun _ ha ↦ mem_nonZeroDivisors_of_injective hf (Submonoid.mem_comap.mp ha)
 
 @[deprecated (since := "2025-02-03")]
 alias comap_nonZeroDivisor_le_of_injective := comap_nonZeroDivisors_le_of_injective
 
 end MonoidWithZero
 
+section CommMonoidWithZero
+variable {M₀ : Type*} [CommMonoidWithZero M₀] {a b r x : M₀}
+
+lemma mul_left_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : r * x = 0 ↔ x = 0 := by
+  rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
+
+@[simp]
+lemma mul_left_coe_nonZeroDivisors_eq_zero_iff {c : M₀⁰} : (c : M₀) * x = 0 ↔ x = 0 :=
+  mul_left_mem_nonZeroDivisors_eq_zero_iff c.prop
+
+lemma mul_mem_nonZeroDivisors : a * b ∈ M₀⁰ ↔ a ∈ M₀⁰ ∧ b ∈ M₀⁰ where
+  mp h := by
+    constructor <;> intro x h' <;> apply h
+    · rw [← mul_assoc, h', zero_mul]
+    · rw [mul_comm a b, ← mul_assoc, h', zero_mul]
+  mpr := by
+    rintro ⟨ha, hb⟩ x hx
+    apply ha
+    apply hb
+    rw [mul_assoc, hx]
+
+end CommMonoidWithZero
+
 section GroupWithZero
 variable {G₀ : Type*} [GroupWithZero G₀] {x : G₀}
 
@@ -248,21 +260,21 @@ section nonZeroSMulDivisors
 
 open nonZeroSMulDivisors nonZeroDivisors
 
-variable {R M : Type*} [MonoidWithZero R] [Zero M] [MulAction R M]
+variable {M₀ M : Type*} [MonoidWithZero M₀] [Zero M] [MulAction M₀ M] {x : M₀}
 
-lemma mem_nonZeroSMulDivisors_iff {x : R} : x ∈ R⁰[M] ↔ ∀ (m : M), x • m = 0 → m = 0 := Iff.rfl
+lemma mem_nonZeroSMulDivisors_iff : x ∈ M₀⁰[M] ↔ ∀ (m : M), x • m = 0 → m = 0 := Iff.rfl
 
-variable (R)
+variable (M₀)
 
 @[simp]
 lemma unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors :
-    (Rᵐᵒᵖ ⁰[R]).unop = R⁰ := rfl
+    (M₀ᵐᵒᵖ ⁰[M₀]).unop = M₀⁰ := 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
+    M₀ᵐᵒᵖ ⁰[M₀] = M₀⁰.op := rfl
 
 end nonZeroSMulDivisors