[Merged by Bors] - refactor: move the definition of IsRegular earlier

Mathlib.lean

@@ -469,6 +469,7 @@ import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
 import Mathlib.Algebra.GroupWithZero.Prod
 import Mathlib.Algebra.GroupWithZero.ProdHom
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Subgroup
 import Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

Mathlib/Algebra/GroupWithZero/Regular.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2021 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import Mathlib.Algebra.Regular.Basic
+import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Tactic.Push
+
+/-!
+# Results about `IsRegular` and `0`
+-/
+
+variable {R}
+
+section MulZeroClass
+variable [MulZeroClass R] {a b : R}
+
+/-- The element `0` is left-regular if and only if `R` is trivial. -/
+theorem IsLeftRegular.subsingleton (h : IsLeftRegular (0 : R)) : Subsingleton R :=
+  ⟨fun a b => h <| Eq.trans (zero_mul a) (zero_mul b).symm⟩
+
+/-- The element `0` is right-regular if and only if `R` is trivial. -/
+theorem IsRightRegular.subsingleton (h : IsRightRegular (0 : R)) : Subsingleton R :=
+  ⟨fun a b => h <| Eq.trans (mul_zero a) (mul_zero b).symm⟩
+
+/-- The element `0` is regular if and only if `R` is trivial. -/
+theorem IsRegular.subsingleton (h : IsRegular (0 : R)) : Subsingleton R :=
+  h.left.subsingleton
+
+/-- The element `0` is left-regular if and only if `R` is trivial. -/
+theorem isLeftRegular_zero_iff_subsingleton : IsLeftRegular (0 : R) ↔ Subsingleton R :=
+  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
+
+/-- In a non-trivial `MulZeroClass`, the `0` element is not left-regular. -/
+theorem not_isLeftRegular_zero_iff : ¬IsLeftRegular (0 : R) ↔ Nontrivial R := by
+  rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
+  push_neg
+  exact Iff.rfl
+
+/-- The element `0` is right-regular if and only if `R` is trivial. -/
+theorem isRightRegular_zero_iff_subsingleton : IsRightRegular (0 : R) ↔ Subsingleton R :=
+  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
+
+/-- In a non-trivial `MulZeroClass`, the `0` element is not right-regular. -/
+theorem not_isRightRegular_zero_iff : ¬IsRightRegular (0 : R) ↔ Nontrivial R := by
+  rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
+  push_neg
+  exact Iff.rfl
+
+/-- The element `0` is regular if and only if `R` is trivial. -/
+theorem isRegular_iff_subsingleton : IsRegular (0 : R) ↔ Subsingleton R :=
+  ⟨fun h => h.left.subsingleton, fun h =>
+    ⟨isLeftRegular_zero_iff_subsingleton.mpr h, isRightRegular_zero_iff_subsingleton.mpr h⟩⟩
+
+/-- A left-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
+theorem IsLeftRegular.ne_zero [Nontrivial R] (la : IsLeftRegular a) : a ≠ 0 := by
+  rintro rfl
+  rcases exists_pair_ne R with ⟨x, y, xy⟩
+  refine xy (la (?_ : 0 * x = 0 * y)) -- Porting note: lean4 seems to need the type signature
+  rw [zero_mul, zero_mul]
+
+/-- A right-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
+theorem IsRightRegular.ne_zero [Nontrivial R] (ra : IsRightRegular a) : a ≠ 0 := by
+  rintro rfl
+  rcases exists_pair_ne R with ⟨x, y, xy⟩
+  refine xy (ra (?_ : x * 0 = y * 0))
+  rw [mul_zero, mul_zero]
+
+/-- A regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
+theorem IsRegular.ne_zero [Nontrivial R] (la : IsRegular a) : a ≠ 0 :=
+  la.left.ne_zero
+
+/-- In a non-trivial ring, the element `0` is not left-regular -- with typeclasses. -/
+theorem not_isLeftRegular_zero [nR : Nontrivial R] : ¬IsLeftRegular (0 : R) :=
+  not_isLeftRegular_zero_iff.mpr nR
+
+/-- In a non-trivial ring, the element `0` is not right-regular -- with typeclasses. -/
+theorem not_isRightRegular_zero [nR : Nontrivial R] : ¬IsRightRegular (0 : R) :=
+  not_isRightRegular_zero_iff.mpr nR
+
+/-- In a non-trivial ring, the element `0` is not regular -- with typeclasses. -/
+theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRegular.ne_zero h rfl
+
+@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
+  conv_lhs => rw [← mul_zero b]
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
+
+@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
+  conv_lhs => rw [← zero_mul b]
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
+
+end MulZeroClass
+
+section CancelMonoidWithZero
+variable [MulZeroClass R] [IsCancelMulZero R] {a : R}
+
+/-- Non-zero elements of an integral domain are regular. -/
+theorem isRegular_of_ne_zero (a0 : a ≠ 0) : IsRegular a :=
+  ⟨fun _ _ => mul_left_cancel₀ a0, fun _ _ => mul_right_cancel₀ a0⟩
+
+/-- In a non-trivial integral domain, an element is regular iff it is non-zero. -/
+theorem isRegular_iff_ne_zero [Nontrivial R] : IsRegular a ↔ a ≠ 0 :=
+  ⟨IsRegular.ne_zero, isRegular_of_ne_zero⟩
+
+end CancelMonoidWithZero

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -3,10 +3,10 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Anne Baanen
 -/
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Algebra.Regular.Basic
 import Mathlib.Tactic.Positivity.Core
 
 /-!

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Data.Ordering.Basic
 import Mathlib.Order.MinMax
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Use
+import Mathlib.Algebra.Regular.Basic
 
 /-!
 # Ordered monoids
@@ -1366,6 +1367,11 @@ protected theorem Injective [Mul α] [PartialOrder α] {a : α} (ha : MulLECance
     Injective (a * ·) :=
   fun _ _ h => le_antisymm (ha h.le) (ha h.ge)
 
+@[to_additive]
+protected theorem isLeftRegular [Mul α] [PartialOrder α] {a : α}
+    (ha : MulLECancellable a) : IsLeftRegular a :=
+  ha.Injective
+
 @[to_additive]
 protected theorem inj [Mul α] [PartialOrder α] {a b c : α} (ha : MulLECancellable a) :
     a * b = a * c ↔ b = c :=

Mathlib/Algebra/Order/Star/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.Opposite

Mathlib/Algebra/Polynomial/Degree/Operations.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.Polynomial.Coeff
 import Mathlib.Algebra.Polynomial.Degree.Definitions
 

Mathlib/Algebra/Regular/Basic.lean

@@ -3,11 +3,9 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
+import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Commute.Defs
 import Mathlib.Algebra.Group.Units.Defs
-import Mathlib.Algebra.GroupWithZero.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
-import Mathlib.Tactic.NthRewrite
 
 /-!
 # Regular elements
@@ -72,18 +70,13 @@ attribute [to_additive] IsRegular
 theorem isRegular_iff {c : R} : IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c :=
   ⟨fun ⟨h1, h2⟩ => ⟨h1, h2⟩, fun ⟨h1, h2⟩ => ⟨h1, h2⟩⟩
 
-@[to_additive]
-protected theorem MulLECancellable.isLeftRegular [PartialOrder R] {a : R}
-    (ha : MulLECancellable a) : IsLeftRegular a :=
-  ha.Injective
-
 theorem IsLeftRegular.right_of_commute {a : R}
     (ca : ∀ b, Commute a b) (h : IsLeftRegular a) : IsRightRegular a :=
   fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
 
 theorem IsRightRegular.left_of_commute {a : R}
     (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a := by
-  simp_rw [@Commute.symm_iff R _ a] at ca
+  simp only [@Commute.symm_iff R _ a] at ca
   exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
 
 theorem Commute.isRightRegular_iff {a : R} (ca : ∀ b, Commute a b) :
@@ -173,85 +166,6 @@ theorem IsRegular.and_of_mul_of_mul (ab : IsRegular (a * b)) (ba : IsRegular (b
 
 end Semigroup
 
-section MulZeroClass
-
-variable [MulZeroClass R] {a b : R}
-
-/-- The element `0` is left-regular if and only if `R` is trivial. -/
-theorem IsLeftRegular.subsingleton (h : IsLeftRegular (0 : R)) : Subsingleton R :=
-  ⟨fun a b => h <| Eq.trans (zero_mul a) (zero_mul b).symm⟩
-
-/-- The element `0` is right-regular if and only if `R` is trivial. -/
-theorem IsRightRegular.subsingleton (h : IsRightRegular (0 : R)) : Subsingleton R :=
-  ⟨fun a b => h <| Eq.trans (mul_zero a) (mul_zero b).symm⟩
-
-/-- The element `0` is regular if and only if `R` is trivial. -/
-theorem IsRegular.subsingleton (h : IsRegular (0 : R)) : Subsingleton R :=
-  h.left.subsingleton
-
-/-- The element `0` is left-regular if and only if `R` is trivial. -/
-theorem isLeftRegular_zero_iff_subsingleton : IsLeftRegular (0 : R) ↔ Subsingleton R :=
-  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
-
-/-- In a non-trivial `MulZeroClass`, the `0` element is not left-regular. -/
-theorem not_isLeftRegular_zero_iff : ¬IsLeftRegular (0 : R) ↔ Nontrivial R := by
-  rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
-  push_neg
-  exact Iff.rfl
-
-/-- The element `0` is right-regular if and only if `R` is trivial. -/
-theorem isRightRegular_zero_iff_subsingleton : IsRightRegular (0 : R) ↔ Subsingleton R :=
-  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
-
-/-- In a non-trivial `MulZeroClass`, the `0` element is not right-regular. -/
-theorem not_isRightRegular_zero_iff : ¬IsRightRegular (0 : R) ↔ Nontrivial R := by
-  rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
-  push_neg
-  exact Iff.rfl
-
-/-- The element `0` is regular if and only if `R` is trivial. -/
-theorem isRegular_iff_subsingleton : IsRegular (0 : R) ↔ Subsingleton R :=
-  ⟨fun h => h.left.subsingleton, fun h =>
-    ⟨isLeftRegular_zero_iff_subsingleton.mpr h, isRightRegular_zero_iff_subsingleton.mpr h⟩⟩
-
-/-- A left-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
-theorem IsLeftRegular.ne_zero [Nontrivial R] (la : IsLeftRegular a) : a ≠ 0 := by
-  rintro rfl
-  rcases exists_pair_ne R with ⟨x, y, xy⟩
-  refine xy (la (?_ : 0 * x = 0 * y)) -- Porting note: lean4 seems to need the type signature
-  rw [zero_mul, zero_mul]
-
-/-- A right-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
-theorem IsRightRegular.ne_zero [Nontrivial R] (ra : IsRightRegular a) : a ≠ 0 := by
-  rintro rfl
-  rcases exists_pair_ne R with ⟨x, y, xy⟩
-  refine xy (ra (?_ : x * 0 = y * 0))
-  rw [mul_zero, mul_zero]
-
-/-- A regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
-theorem IsRegular.ne_zero [Nontrivial R] (la : IsRegular a) : a ≠ 0 :=
-  la.left.ne_zero
-
-/-- In a non-trivial ring, the element `0` is not left-regular -- with typeclasses. -/
-theorem not_isLeftRegular_zero [nR : Nontrivial R] : ¬IsLeftRegular (0 : R) :=
-  not_isLeftRegular_zero_iff.mpr nR
-
-/-- In a non-trivial ring, the element `0` is not right-regular -- with typeclasses. -/
-theorem not_isRightRegular_zero [nR : Nontrivial R] : ¬IsRightRegular (0 : R) :=
-  not_isRightRegular_zero_iff.mpr nR
-
-/-- In a non-trivial ring, the element `0` is not regular -- with typeclasses. -/
-theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRegular.ne_zero h rfl
-
-@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
-  nth_rw 1 [← mul_zero b]
-  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
-
-@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
-  nth_rw 1 [← zero_mul b]
-  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
-
-end MulZeroClass
 
 section MulOneClass
 
@@ -346,17 +260,3 @@ theorem IsRightRegular.all [Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular
 @[to_additive "If all additions cancel then every element is add-regular."]
 theorem IsRegular.all [Mul R] [IsCancelMul R] (g : R) : IsRegular g :=
   ⟨mul_right_injective g, mul_left_injective g⟩
-
-section CancelMonoidWithZero
-
-variable [MulZeroClass R] [IsCancelMulZero R] {a : R}
-
-/-- Non-zero elements of an integral domain are regular. -/
-theorem isRegular_of_ne_zero (a0 : a ≠ 0) : IsRegular a :=
-  ⟨fun _ _ => mul_left_cancel₀ a0, fun _ _ => mul_right_cancel₀ a0⟩
-
-/-- In a non-trivial integral domain, an element is regular iff it is non-zero. -/
-theorem isRegular_iff_ne_zero [Nontrivial R] : IsRegular a ↔ a ≠ 0 :=
-  ⟨IsRegular.ne_zero, isRegular_of_ne_zero⟩
-
-end CancelMonoidWithZero

Mathlib/Algebra/Ring/Regular.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
 -/
-import Mathlib.Algebra.Regular.Basic
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.Ring.Defs
 
 /-!

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Scott Carnahan
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Lattice
+import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Data.Finset.MulAntidiagonal
 import Mathlib.Data.Finset.SMulAntidiagonal