[Merged by Bors] - chore(algebra/ring): move some classes to group_with_zero

src/algebra/char_p.lean

@@ -212,7 +212,7 @@ assume (d : ℕ) (hdvd : ∃ e, p = d * e),
 let ⟨e, hmul⟩ := hdvd in
 have (p : α) = 0, from (cast_eq_zero_iff α p p).mpr (dvd_refl p),
 have (d : α) * e = 0, from (@cast_mul α _ d e) ▸ (hmul ▸ this),
-or.elim (no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero (d : α) e this)
+or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this)
   (assume hd : (d : α) = 0,
   have p ∣ d, from (cast_eq_zero_iff α p d).mp hd,
   show d = 1 ∨ d = p, from or.inr (dvd_antisymm ⟨e, hmul⟩ this))

src/algebra/group_with_zero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import algebra.group.commute
-import algebra.ring
+import tactic.alias
 import tactic.push_neg
 
 /-!
@@ -34,6 +34,89 @@ and require `0⁻¹ = 0`.
 
 set_option old_structure_cmd true
 
+variables {G₀ : Type*}
+
+mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to
+reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
+division-free."
+
+section
+set_option default_priority 100 -- see Note [default priority]
+
+@[protect_proj, ancestor has_mul has_zero]
+class mul_zero_class (G₀ : Type*) extends has_mul G₀, has_zero G₀ :=
+(zero_mul : ∀ a : G₀, 0 * a = 0)
+(mul_zero : ∀ a : G₀, a * 0 = 0)
+
+@[ematch, simp] lemma zero_mul [mul_zero_class G₀] (a : G₀) : 0 * a = 0 :=
+mul_zero_class.zero_mul a
+
+@[ematch, simp] lemma mul_zero [mul_zero_class G₀] (a : G₀) : a * 0 = 0 :=
+mul_zero_class.mul_zero a
+
+/-- Predicate typeclass for expressing that a (semi)ring or similar algebraic structure
+is nonzero. -/
+@[protect_proj] class nonzero (G₀ : Type*) [has_zero G₀] [has_one G₀] : Prop :=
+(zero_ne_one : 0 ≠ (1:G₀))
+
+@[simp]
+lemma zero_ne_one [has_zero G₀] [has_one G₀] [nonzero G₀] : 0 ≠ (1:G₀) :=
+nonzero.zero_ne_one
+
+@[simp]
+lemma one_ne_zero [has_zero G₀] [has_one G₀] [nonzero G₀] : (1:G₀) ≠ 0 :=
+zero_ne_one.symm
+
+class no_zero_divisors (G₀ : Type*) [has_mul G₀] [has_zero G₀] : Prop :=
+(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : G₀}, a * b = 0 → a = 0 ∨ b = 0)
+
+export no_zero_divisors (eq_zero_or_eq_zero_of_mul_eq_zero)
+
+lemma eq_zero_of_mul_self_eq_zero [has_mul G₀] [has_zero G₀] [no_zero_divisors G₀] {a : G₀}
+  (h : a * a = 0) :
+  a = 0 :=
+or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) (assume h', h') (assume h', h')
+
+section
+
+variables [mul_zero_class G₀] [no_zero_divisors G₀] {a b : G₀}
+
+/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
+equals zero. -/
+@[simp] theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=
+⟨eq_zero_or_eq_zero_of_mul_eq_zero, λo,
+  or.elim o (λh, by rw h; apply zero_mul) (λh, by rw h; apply mul_zero)⟩
+
+/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
+equals zero. -/
+@[simp] theorem zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0 :=
+by rw [eq_comm, mul_eq_zero]
+
+/-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
+are nonzero. -/
+theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 :=
+(not_congr mul_eq_zero).trans not_or_distrib
+
+theorem mul_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
+mul_ne_zero_iff.2 ⟨ha, hb⟩
+
+/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` equals zero iff so is
+`b * a`. -/
+theorem mul_eq_zero_comm : a * b = 0 ↔ b * a = 0 :=
+mul_eq_zero.trans $ (or_comm _ _).trans mul_eq_zero.symm
+
+/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` is nonzero iff so is
+`b * a`. -/
+theorem mul_ne_zero_comm : a * b ≠ 0 ↔ b * a ≠ 0 :=
+not_congr mul_eq_zero_comm
+
+lemma mul_self_eq_zero : a * a = 0 ↔ a = 0 := by simp
+lemma zero_eq_mul_self : 0 = a * a ↔ a = 0 := by simp
+
+end
+
+end -- default_priority 100
+
 section prio
 set_option default_priority 10 -- see Note [default priority]
 
@@ -77,7 +160,7 @@ lemma div_eq_mul_inv {G₀ : Type*} [group_with_zero G₀] {a b : G₀} :
 alias div_eq_mul_inv ← division_def
 
 section group_with_zero
-variables {G₀ : Type*} [group_with_zero G₀]
+variables [group_with_zero G₀]
 
 @[simp] lemma inv_zero : (0 : G₀)⁻¹ = 0 :=
 group_with_zero.inv_zero
@@ -212,7 +295,7 @@ calc 0 = (a : G₀) * a⁻¹ : by simp [a_eq_0]
 end group_with_zero
 
 namespace units
-variables {G₀ : Type*} [group_with_zero G₀]
+variables [group_with_zero G₀]
 variables {a b : G₀}
 
 /-- Embed a non-zero element of a `group_with_zero` into the unit group.
@@ -240,7 +323,7 @@ units.ext rfl
 end units
 
 section group_with_zero
-variables {G₀ : Type*} [group_with_zero G₀]
+variables [group_with_zero G₀]
 
 lemma is_unit.mk0 (x : G₀) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
 
@@ -359,7 +442,7 @@ end group_with_zero
 
 section group_with_zero
 
-variables {G₀ : Type*} [group_with_zero G₀]
+variables [group_with_zero G₀]
 variables {a b c : G₀}
 
 @[simp] lemma inv_eq_zero {a : G₀} : a⁻¹ = 0 ↔ a = 0 :=
@@ -410,7 +493,7 @@ by simp only [div_eq_mul_inv, mul_inv_rev', mul_assoc, mul_inv_cancel_assoc_righ
 end group_with_zero
 
 section comm_group_with_zero -- comm
-variables {G₀ : Type*} [comm_group_with_zero G₀] {a b c : G₀}
+variables [comm_group_with_zero G₀] {a b c : G₀}
 
 lemma mul_inv'' : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
 by rw [mul_inv_rev', mul_comm]
@@ -499,7 +582,7 @@ by rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]
 end comm_group_with_zero
 
 section comm_group_with_zero
-variables {G₀ : Type*} [comm_group_with_zero G₀] {a b c d : G₀}
+variables [comm_group_with_zero G₀] {a b c d : G₀}
 
 lemma div_eq_inv_mul : a / b = b⁻¹ * a := mul_comm _ _
 
@@ -544,7 +627,13 @@ end comm_group_with_zero
 
 namespace semiconj_by
 
-variables {G₀ : Type*} [group_with_zero G₀] {a x y x' y' : G₀}
+@[simp] lemma zero_right [mul_zero_class G₀] (a : G₀) : semiconj_by a 0 0 :=
+by simp only [semiconj_by, mul_zero, zero_mul]
+
+@[simp] lemma zero_left [mul_zero_class G₀] (x y : G₀) : semiconj_by 0 x y :=
+by simp only [semiconj_by, mul_zero, zero_mul]
+
+variables [group_with_zero G₀] {a x y x' y' : G₀}
 
 @[simp] lemma inv_symm_left_iff' : semiconj_by a⁻¹ x y ↔ semiconj_by a y x :=
 classical.by_cases
@@ -579,7 +668,10 @@ end semiconj_by
 
 namespace commute
 
-variables {G₀ : Type*} [group_with_zero G₀] {a b c : G₀}
+@[simp] theorem zero_right [mul_zero_class G₀] (a : G₀) :commute a 0 := semiconj_by.zero_right a
+@[simp] theorem zero_left [mul_zero_class G₀] (a : G₀) : commute 0 a := semiconj_by.zero_left a a
+
+variables [group_with_zero G₀] {a b c : G₀}
 
 @[simp] theorem inv_left_iff' : commute a⁻¹ b ↔ commute a b :=
 semiconj_by.inv_symm_left_iff'

src/algebra/ring.lean

@@ -6,6 +6,7 @@ Neil Strickland
 -/
 import algebra.group.hom
 import algebra.group.units
+import algebra.group_with_zero
 import tactic.alias
 import tactic.norm_cast
 import tactic.split_ifs
@@ -54,49 +55,21 @@ variables {α : Type u} {β : Type v} {γ : Type w} {R : Type x}
 set_option default_priority 100 -- see Note [default priority]
 set_option old_structure_cmd true
 
-mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to
-reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
-division-free."
-
 @[protect_proj, ancestor has_mul has_add]
-class distrib (α : Type u) extends has_mul α, has_add α :=
-(left_distrib : ∀ a b c : α, a * (b + c) = (a * b) + (a * c))
-(right_distrib : ∀ a b c : α, (a + b) * c = (a * c) + (b * c))
+class distrib (R : Type*) extends has_mul R, has_add R :=
+(left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c))
+(right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c))
 
-lemma left_distrib [distrib α] (a b c : α) : a * (b + c) = a * b + a * c :=
+lemma left_distrib [distrib R] (a b c : R) : a * (b + c) = a * b + a * c :=
 distrib.left_distrib a b c
 
 alias left_distrib ← mul_add
 
-lemma right_distrib [distrib α] (a b c : α) : (a + b) * c = a * c + b * c :=
+lemma right_distrib [distrib R] (a b c : R) : (a + b) * c = a * c + b * c :=
 distrib.right_distrib a b c
 
 alias right_distrib ← add_mul
 
-@[protect_proj, ancestor has_mul has_zero]
-class mul_zero_class (α : Type u) extends has_mul α, has_zero α :=
-(zero_mul : ∀ a : α, 0 * a = 0)
-(mul_zero : ∀ a : α, a * 0 = 0)
-
-@[ematch, simp] lemma zero_mul [mul_zero_class α] (a : α) : 0 * a = 0 :=
-mul_zero_class.zero_mul a
-
-@[ematch, simp] lemma mul_zero [mul_zero_class α] (a : α) : a * 0 = 0 :=
-mul_zero_class.mul_zero a
-
-/-- Predicate typeclass for expressing that a (semi)ring or similar algebraic structure
-is nonzero. -/
-@[protect_proj] class nonzero (α : Type u) [has_zero α] [has_one α] : Prop :=
-(zero_ne_one : 0 ≠ (1:α))
-
-@[simp]
-lemma zero_ne_one [has_zero α] [has_one α] [nonzero α] : 0 ≠ (1:α) :=
-nonzero.zero_ne_one
-
-@[simp]
-lemma one_ne_zero [has_zero α] [has_one α] [nonzero α] : (1:α) ≠ 0 :=
-zero_ne_one.symm
-
 /-!
 ### Semirings
 -/
@@ -727,55 +700,6 @@ lemma units.coe_ne_zero [semiring α] [nonzero α] (u : units α) : (u : α) ≠
 theorem nonzero.of_ne [semiring α] {x y : α} (h : x ≠ y) : nonzero α :=
 { zero_ne_one := λ h01, h $ by rw [← one_mul x, ← one_mul y, ← h01, zero_mul, zero_mul] }
 
-@[protect_proj] class no_zero_divisors (α : Type u) [has_mul α] [has_zero α] : Prop :=
-(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
-
-lemma eq_zero_or_eq_zero_of_mul_eq_zero [has_mul α] [has_zero α] [no_zero_divisors α]
-  {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 :=
-no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero a b h
-
-lemma eq_zero_of_mul_self_eq_zero [has_mul α] [has_zero α] [no_zero_divisors α]
-  {a : α} (h : a * a = 0) : a = 0 :=
-or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) (assume h', h') (assume h', h')
-
-section
-
-variables [mul_zero_class α] [no_zero_divisors α]
-
-/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
-equals zero. -/
-@[simp] theorem mul_eq_zero {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
-⟨eq_zero_or_eq_zero_of_mul_eq_zero, λo,
-  or.elim o (λh, by rw h; apply zero_mul) (λh, by rw h; apply mul_zero)⟩
-
-/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
-equals zero. -/
-@[simp] theorem zero_eq_mul {a b : α} : 0 = a * b ↔ a = 0 ∨ b = 0 :=
-by rw [eq_comm, mul_eq_zero]
-
-/-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
-are nonzero. -/
-theorem mul_ne_zero_iff {a b : α} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 :=
-(not_congr mul_eq_zero).trans not_or_distrib
-
-theorem mul_ne_zero {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
-mul_ne_zero_iff.2 ⟨ha, hb⟩
-
-/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` equals zero iff so is
-`b * a`. -/
-theorem mul_eq_zero_comm {a b : α} : a * b = 0 ↔ b * a = 0 :=
-mul_eq_zero.trans $ (or_comm _ _).trans mul_eq_zero.symm
-
-/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` is nonzero iff so is
-`b * a`. -/
-theorem mul_ne_zero_comm {a b : α} : a * b ≠ 0 ↔ b * a ≠ 0 :=
-not_congr mul_eq_zero_comm
-
-lemma mul_self_eq_zero {x : α} : x * x = 0 ↔ x = 0 := by simp
-lemma zero_eq_mul_self {x : α} : 0 = x * x ↔ x = 0 := by simp
-
-end
-
 /-- A domain is a ring with no zero divisors, i.e. satisfying
   the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
   is an integral domain without assuming commutativity of multiplication. -/
@@ -971,14 +895,6 @@ by simp only [semiconj_by, left_distrib, right_distrib, h.eq, h'.eq]
   semiconj_by (a + b) x y :=
 by simp only [semiconj_by, left_distrib, right_distrib, ha.eq, hb.eq]
 
-@[simp] lemma zero_right [mul_zero_class R] (a : R) :
-  semiconj_by a 0 0 :=
-by simp only [semiconj_by, mul_zero, zero_mul]
-
-@[simp] lemma zero_left [mul_zero_class R] (x y : R) :
-  semiconj_by 0 x y :=
-by simp only [semiconj_by, mul_zero, zero_mul]
-
 variables [ring R] {a b x y x' y' : R}
 
 lemma neg_right (h : semiconj_by a x y) : semiconj_by a (-x) (-y) :=
@@ -1019,9 +935,6 @@ semiconj_by.add_right
   commute a c → commute b c → commute (a + b) c :=
 semiconj_by.add_left
 
-@[simp] theorem zero_right [mul_zero_class R] (a : R) :commute a 0 := semiconj_by.zero_right a
-@[simp] theorem zero_left [mul_zero_class R] (a : R) : commute 0 a := semiconj_by.zero_left a a
-
 variables [ring R] {a b c : R}
 
 theorem neg_right : commute a b → commute a (- b) := semiconj_by.neg_right

src/data/real/hyperreal.lean

@@ -508,8 +508,7 @@ is_st_iff_abs_sub_lt_delta.mpr $ λ d hd,
   ... = (d / 2 * (abs x / t) + d / 2 : ℝ*) : by
       { push_cast,
         have : (abs s : ℝ*) ≠ 0, by simpa,
-        field_simp [this, @two_ne_zero ℝ* _, add_mul, mul_add],
-        congr' 1; ac_refl }
+        field_simp [this, @two_ne_zero ℝ* _, add_mul, mul_add, mul_assoc, mul_comm, mul_left_comm] }
   ... < (d / 2 * 1 + d / 2 : ℝ*) :
         add_lt_add_right (mul_lt_mul_of_pos_left
         ((div_lt_one_iff_lt $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $

src/ring_theory/free_comm_ring.lean

@@ -69,7 +69,7 @@ free_abelian_group.lift.sub _ _ _
 @[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
 begin
   refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
-  { intros s2, conv { to_lhs, dsimp only [(*), mul_zero_class.mul, semiring.mul, ring.mul, semigroup.mul, comm_ring.mul] },
+  { intros s2, conv_lhs { dsimp only [(*), distrib.mul, ring.mul, comm_ring.mul, semigroup.mul] },
     rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
     refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
     { intros s1, iterate 3 { rw free_abelian_group.lift.of },

src/ring_theory/free_ring.lean

@@ -62,7 +62,7 @@ free_abelian_group.lift.sub _ _ _
 @[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
 begin
   refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
-  { intros L2, conv { to_lhs, dsimp only [(*), mul_zero_class.mul, semiring.mul, ring.mul, semigroup.mul] },
+  { intros L2, conv_lhs { dsimp only [(*), distrib.mul, ring.mul, semigroup.mul] },
     rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
     refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
     { intros L1, iterate 3 { rw free_abelian_group.lift.of },