refactor(algebra/*): small API fixes (#3157)

## Changes to `canonically_ordered_comm_semiring`

* in the definition of `canonically_ordered_comm_semiring` replace
  `mul_eq_zero_iff` with `eq_zero_or_eq_zero_of_mul_eq_zero`; the other
  implication is always true because of `[semiring]`;
* add instance `canonically_ordered_comm_semiring.to_no_zero_divisors`;

## Changes to `with_top`

* use `to_additive` for `with_top.has_one`, `with_top.coe_one` etc;
* move `with_top.coe_ne_zero` to `algebra.ordered_group`;
* add `with_top.has_add`, make `coe_add`, `coe_bit*` require only `[has_add α]`;
* use proper instances for lemmas about multiplication in `with_top`, not
  just `canonically_ordered_comm_semiring` for everything;

## Changes to `associates`
* merge `associates.mk_zero_eq` and `associates.mk_eq_zero_iff_eq_zero` into
  `associates.mk_eq_zero`;
* drop `associates.mul_zero`, `associates.zero_mul`, `associates.zero_ne_one`,
  and `associates.mul_eq_zero_iff` in favor of typeclass instances;

## Misc changes

* drop `mul_eq_zero_iff_eq_zero_or_eq_zero` in favor of `mul_eq_zero`;
* drop `ennreal.mul_eq_zero` in favor of `mul_eq_zero` from instance.

Author: urkud

src/algebra/associated.lean

@@ -441,18 +441,14 @@ instance [has_zero α] [monoid α] : has_top (associates α) := ⟨0⟩
 section comm_semiring
 variables [comm_semiring α]
 
-@[simp] theorem mk_zero_eq (a : α) : associates.mk a = 0 ↔ a = 0 :=
+@[simp] theorem mk_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
 ⟨assume h, (associated_zero_iff_eq_zero a).1 $ quotient.exact h, assume h, h.symm ▸ rfl⟩
 
-@[simp] theorem mul_zero : ∀(a : associates α), a * 0 = 0 :=
-by rintros ⟨a⟩; show associates.mk (a * 0) = associates.mk 0; rw [mul_zero]
-
-@[simp] protected theorem zero_mul : ∀(a : associates α), 0 * a = 0 :=
-by rintros ⟨a⟩; show associates.mk (0 * a) = associates.mk 0; rw [zero_mul]
-
-theorem mk_eq_zero_iff_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
-calc associates.mk a = 0 ↔ (a ~ᵤ 0) :  mk_eq_mk_iff_associated
-  ... ↔ a = 0 : associated_zero_iff_eq_zero a
+instance : mul_zero_class (associates α) :=
+{ mul := (*),
+  zero := 0,
+  zero_mul := by { rintro ⟨a⟩, show associates.mk (0 * a) = associates.mk 0, rw [zero_mul] },
+  mul_zero := by { rintro ⟨a⟩, show associates.mk (a * 0) = associates.mk 0, rw [mul_zero] } }
 
 theorem dvd_of_mk_le_mk {a b : α} : associates.mk a ≤ associates.mk b → a ∣ b
 | ⟨c', hc'⟩ := (quotient.induction_on c' $ assume c hc,
@@ -499,7 +495,7 @@ begin
     apply forall_congr, assume a,
     exact forall_associated },
   apply and_congr,
-  { rw [(≠), mk_zero_eq] },
+  { rw [(≠), mk_eq_zero] },
   apply and_congr,
   { rw [(≠), ← is_unit_iff_eq_one, is_unit_mk], },
   apply forall_congr, assume a,
@@ -532,24 +528,23 @@ instance : order_top (associates α) :=
   le_top := assume a, ⟨0, mul_zero a⟩,
   .. associates.partial_order }
 
-theorem zero_ne_one : (0 : associates α) ≠ 1 :=
-assume h,
-have (0 : α) ~ᵤ 1, from quotient.exact h,
-have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
-zero_ne_one this
+instance : nonzero (associates α) :=
+⟨ assume h,
+  have (0 : α) ~ᵤ 1, from quotient.exact h,
+  have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
+  zero_ne_one this ⟩
 
-theorem mul_eq_zero_iff {x y : associates α} : x * y = 0 ↔ x = 0 ∨ y = 0 :=
-iff.intro
+instance : no_zero_divisors (associates α) :=
+⟨λ x y,
   (quotient.induction_on₂ x y $ assume a b h,
     have a * b = 0, from (associated_zero_iff_eq_zero _).1 (quotient.exact h),
-    have a = 0 ∨ b = 0, from mul_eq_zero_iff_eq_zero_or_eq_zero.1 this,
-    this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))
-  (by simp [or_imp_distrib] {contextual := tt})
+    have a = 0 ∨ b = 0, from mul_eq_zero.1 this,
+    this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))⟩
 
 theorem prod_eq_zero_iff {s : multiset (associates α)} :
   s.prod = 0 ↔ (0 : associates α) ∈ s :=
 multiset.induction_on s (by simp; exact zero_ne_one.symm) $
-  assume a s, by simp [mul_eq_zero_iff, @eq_comm _ 0 a] {contextual := tt}
+  assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
 
 theorem irreducible_mk_iff (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
 begin
@@ -573,7 +568,7 @@ begin
   rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
   rcases quotient.exact' h with ⟨u, hu⟩,
   have hu : a * (b * ↑u) = a * c, { rwa [← mul_assoc] },
-  exact quotient.sound' ⟨u, eq_of_mul_eq_mul_left (mt (mk_zero_eq a).2 ha) hu⟩
+  exact quotient.sound' ⟨u, eq_of_mul_eq_mul_left (mt mk_eq_zero.2 ha) hu⟩
 end
 
 lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :

src/algebra/big_operators.lean

@@ -1098,7 +1098,7 @@ begin
   apply finset.induction_on s,
   exact ⟨not.elim one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩,
   assume a s ha ih,
-  rw [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero, bex_def, exists_mem_insert, ih, ← bex_def]
+  rw [prod_insert ha, mul_eq_zero, bex_def, exists_mem_insert, ih, ← bex_def]
 end
 
 theorem prod_ne_zero_iff : (∏ x in s, f x) ≠ 0 ↔ (∀ a ∈ s, f a ≠ 0) :=

src/algebra/ordered_group.lean

@@ -286,35 +286,40 @@ end with_zero
 
 namespace with_top
 
-instance [has_zero α] : has_zero (with_top α) := ⟨(0 : α)⟩
+section has_one
 
-@[simp, norm_cast] lemma coe_zero {α : Type*}
-  [has_zero α] : ((0 : α) : with_top α) = 0 := rfl
+variables [has_one α]
 
-@[simp, norm_cast] lemma coe_eq_zero {α : Type*}
-  [has_zero α] {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
-by norm_cast
+@[to_additive] instance : has_one (with_top α) := ⟨(1 : α)⟩
 
-instance [has_one α] : has_one (with_top α) := ⟨(1 : α)⟩
+@[simp, to_additive] lemma coe_one : ((1 : α) : with_top α) = 1 := rfl
 
-@[simp, norm_cast] lemma coe_one {α : Type*}
-  [has_one α] : ((1 : α) : with_top α) = 1 := rfl
+@[simp, to_additive] lemma coe_eq_one {a : α} : (a : with_top α) = 1 ↔ a = 1 :=
+coe_eq_coe
 
-@[simp, norm_cast] lemma coe_eq_one {α : Type*}
-  [has_one α] {a : α} : (a : with_top α) = 1 ↔ a = 1 :=
-by norm_cast
+@[simp, to_additive] theorem one_eq_coe {a : α} : 1 = (a : with_top α) ↔ a = 1 :=
+by rw [eq_comm, coe_eq_one]
+
+attribute [norm_cast] coe_one coe_eq_one coe_zero coe_eq_zero one_eq_coe zero_eq_coe
+
+@[simp, to_additive] theorem top_ne_one : ⊤ ≠ (1 : with_top α) .
+@[simp, to_additive] theorem one_ne_top : (1 : with_top α) ≠ ⊤ .
+
+end has_one
+
+instance [has_add α] : has_add (with_top α) :=
+⟨λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b))⟩
 
 instance [add_semigroup α] : add_semigroup (with_top α) :=
-{ add := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b)),
+{ add := (+),
   ..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
 
-@[norm_cast] lemma coe_add [add_semigroup α] {a b : α} : ((a + b : α) : with_top α) = a + b := rfl
+@[norm_cast] lemma coe_add [has_add α] {a b : α} : ((a + b : α) : with_top α) = a + b := rfl
 
-@[norm_cast] lemma coe_bit0 [add_semigroup α] {a : α} : ((bit0 a : α) : with_top α) = bit0 a :=
-by unfold bit0; norm_cast
+@[norm_cast] lemma coe_bit0 [has_add α] {a : α} : ((bit0 a : α) : with_top α) = bit0 a := rfl
 
-@[norm_cast] lemma coe_bit1 [add_semigroup α] [has_one α] {a : α} : ((bit1 a : α) : with_top α) = bit1 a :=
-by unfold bit1; norm_cast
+@[norm_cast]
+lemma coe_bit1 [has_add α] [has_one α] {a : α} : ((bit1 a : α) : with_top α) = bit1 a := rfl
 
 instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
 { ..@additive.add_comm_semigroup _ $

src/algebra/ordered_ring.lean

@@ -928,7 +928,7 @@ in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by t
 natural numbers, for example, but not the integers or other ordered groups. -/
 class canonically_ordered_comm_semiring (α : Type*) extends
   canonically_ordered_add_monoid α, comm_semiring α :=
-(mul_eq_zero_iff (a b : α) : a * b = 0 ↔ a = 0 ∨ b = 0)
+(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
 (zero_ne_one : (0 : α) ≠ 1)
 
 namespace canonically_ordered_semiring
@@ -939,6 +939,10 @@ open canonically_ordered_add_monoid (le_iff_exists_add)
 instance canonically_ordered_comm_semiring.to_nonzero : nonzero α :=
 ⟨canonically_ordered_comm_semiring.zero_ne_one⟩
 
+instance canonically_ordered_comm_semiring.to_no_zero_divisors :
+  no_zero_divisors α :=
+⟨canonically_ordered_comm_semiring.eq_zero_or_eq_zero_of_mul_eq_zero⟩
+
 lemma mul_le_mul {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
   a * c ≤ b * d :=
 begin
@@ -952,22 +956,21 @@ end
 lemma zero_lt_one : (0:α) < 1 := lt_of_le_of_ne (zero_le 1) zero_ne_one
 
 lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
-by simp only [zero_lt_iff_ne_zero, ne.def, canonically_ordered_comm_semiring.mul_eq_zero_iff,
-  not_or_distrib]
+by simp only [zero_lt_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 end canonically_ordered_semiring
 
 namespace with_top
-variables [canonically_ordered_comm_semiring α]
 
-@[simp] theorem top_ne_zero : ⊤ ≠ (0 : with_top α) .
-@[simp] theorem zero_ne_top : (0 : with_top α) ≠ ⊤ .
-
-@[simp] theorem zero_eq_coe {a : α} : 0 = (a : with_top α) ↔ a = 0 :=
-by rw [eq_comm, coe_eq_zero]
+instance [has_zero α] [has_one α] [nonzero α] : nonzero (with_top α) :=
+⟨mt coe_eq_coe.1 zero_ne_one⟩
 
 variable [decidable_eq α]
 
+section has_mul
+
+variables [has_zero α] [has_mul α]
+
 instance : mul_zero_class (with_top α) :=
 { zero := 0,
   mul := λm n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
@@ -986,7 +989,13 @@ by cases a; simp [mul_def, h]; refl
 @[simp] lemma top_mul_top : (⊤ * ⊤ : with_top α) = ⊤ :=
 top_mul top_ne_zero
 
-lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
+end has_mul
+
+section mul_zero_class
+
+variables [mul_zero_class α]
+
+@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
 decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
 decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
 by simp [*, mul_def]; refl
@@ -996,22 +1005,38 @@ lemma mul_coe {b : α} (hb : b ≠ 0) : ∀{a : with_top α}, a * b = a.bind (λ
     by simp [hb]
 | (some a) := show ↑a * ↑b = ↑(a * b), from coe_mul.symm
 
+@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+begin
+  cases a; cases b; simp only [none_eq_top, some_eq_coe],
+  { simp [← coe_mul] },
+  { suffices : ⊤ * (b : with_top α) = ⊤ ↔ b ≠ 0, by simpa,
+    by_cases hb : b = 0; simp [hb] },
+  { suffices : (a : with_top α) * ⊤ = ⊤ ↔ a ≠ 0, by simpa,
+    by_cases ha : a = 0; simp [ha] },
+  { simp [← coe_mul] }
+end
+
+end mul_zero_class
+
+section no_zero_divisors
+
+variables [mul_zero_class α] [no_zero_divisors α]
+
+instance : no_zero_divisors (with_top α) :=
+⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
+  simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
+
+end no_zero_divisors
+
+variables [canonically_ordered_comm_semiring α]
+
 private lemma comm (a b : with_top α) : a * b = b * a :=
 begin
   by_cases ha : a = 0, { simp [ha] },
   by_cases hb : b = 0, { simp [hb] },
   simp [ha, hb, mul_def, option.bind_comm a b, mul_comm]
 end
 
-@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
-begin
-  have H : ∀x:α, (¬x = 0) ↔ (⊤ : with_top α) * ↑x = ⊤ :=
-    λx, ⟨λhx, by simp [top_mul, hx], λhx f, by simpa [f] using hx⟩,
-  cases a; cases b; simp [none_eq_top, top_mul, coe_ne_top, some_eq_coe, coe_mul.symm],
-  { rw [H b] },
-  { rw [H a, comm] }
-end
-
 private lemma distrib' (a b c : with_top α) : (a + b) * c = a * c + b * c :=
 begin
   cases c,
@@ -1023,21 +1048,17 @@ begin
     repeat { refl <|> exact congr_arg some (add_mul _ _ _) } }
 end
 
-private lemma mul_eq_zero (a b : with_top α) : a * b = 0 ↔ a = 0 ∨ b = 0 :=
-by cases a; cases b; dsimp [mul_def]; split_ifs;
-  simp [*, none_eq_top, some_eq_coe, canonically_ordered_comm_semiring.mul_eq_zero_iff] at *
-
 private lemma assoc (a b c : with_top α) : (a * b) * c = a * (b * c) :=
 begin
   cases a,
   { by_cases hb : b = 0; by_cases hc : c = 0;
-      simp [*, none_eq_top, mul_eq_zero b c] },
+      simp [*, none_eq_top] },
   cases b,
   { by_cases ha : a = 0; by_cases hc : c = 0;
-      simp [*, none_eq_top, some_eq_coe, mul_eq_zero ↑a c] },
+      simp [*, none_eq_top, some_eq_coe] },
   cases c,
   { by_cases ha : a = 0; by_cases hb : b = 0;
-      simp [*, none_eq_top, some_eq_coe, mul_eq_zero ↑a ↑b] },
+      simp [*, none_eq_top, some_eq_coe] },
   simp [some_eq_coe, coe_mul.symm, mul_assoc]
 end
 
@@ -1051,10 +1072,9 @@ instance : canonically_ordered_comm_semiring (with_top α) :=
   left_distrib    := assume a b c, by rw [comm, distrib', comm b, comm c]; refl,
   mul_assoc       := assoc,
   mul_comm        := comm,
-  mul_eq_zero_iff := mul_eq_zero,
   one_mul         := one_mul',
   mul_one         := assume a, by rw [comm, one_mul'],
-  zero_ne_one     := assume h : ((0 : α) : with_top α) = 1, zero_ne_one $ option.some.inj h,
-  .. with_top.add_comm_monoid, .. with_top.mul_zero_class, .. with_top.canonically_ordered_add_monoid }
+  .. with_top.add_comm_monoid, .. with_top.mul_zero_class, .. with_top.canonically_ordered_add_monoid,
+  .. with_top.no_zero_divisors, .. with_top.nonzero }
 
 end with_top

src/algebra/ring.lean

@@ -793,13 +793,13 @@ by rw [← sub_eq_zero, ← mul_sub_left_distrib, mul_eq_zero];
 
 /-- An element of a domain fixed by right multiplication by an element other than one must
   be zero. -/
-theorem eq_zero_of_mul_eq_self_right' {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
+theorem eq_zero_of_mul_eq_self_right {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
 by apply (mul_eq_zero.1 _).resolve_right (sub_ne_zero.2 h₁);
     rw [mul_sub_left_distrib, mul_one, sub_eq_zero, h₂]
 
 /-- An element of a domain fixed by left multiplication by an element other than one must
   be zero. -/
-theorem eq_zero_of_mul_eq_self_left' {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 :=
+theorem eq_zero_of_mul_eq_self_left {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 :=
 by apply (mul_eq_zero.1 _).resolve_left (sub_ne_zero.2 h₁);
     rw [mul_sub_right_distrib, one_mul, sub_eq_zero, h₂]
 
@@ -813,34 +813,11 @@ class integral_domain (α : Type u) extends comm_ring α, domain α
 section integral_domain
 variables [integral_domain α] {a b c d e : α}
 
-lemma mul_eq_zero_iff_eq_zero_or_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)⟩
-
 lemma eq_of_mul_eq_mul_right (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
-have b * a - c * a = 0, from sub_eq_zero_of_eq h,
-have (b - c) * a = 0,   by rw [mul_sub_right_distrib, this],
-have b - c = 0,         from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha,
-eq_of_sub_eq_zero this
+(domain.mul_left_inj ha).1 h
 
 lemma eq_of_mul_eq_mul_left (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
-have a * b - a * c = 0, from sub_eq_zero_of_eq h,
-have a * (b - c) = 0,   by rw [mul_sub_left_distrib, this],
-have b - c = 0,         from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha,
-eq_of_sub_eq_zero this
-
-lemma eq_zero_of_mul_eq_self_right (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
-have hb : b - 1 ≠ 0, from
-  assume : b - 1 = 0,
-  have b = 0 + 1, from eq_add_of_sub_eq this,
-  have b = 1,     by rwa zero_add at this,
-  h₁ this,
-have a * b - a = 0,   by simp [h₂],
-have a * (b - 1) = 0, by rwa [mul_sub_left_distrib, mul_one],
-  show a = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hb
-
-lemma eq_zero_of_mul_eq_self_left (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 :=
-eq_zero_of_mul_eq_self_right h₁ (by rwa mul_comm at h₂)
+(domain.mul_right_inj ha).1 h
 
 lemma mul_self_eq_mul_self_iff (a b : α) : a * a = b * b ↔ a = b ∨ a = -b :=
 iff.intro
@@ -861,17 +838,11 @@ by rwa mul_one at this
 
 /-- Right multiplcation by a nonzero element of an integral domain is injective. -/
 theorem eq_of_mul_eq_mul_right_of_ne_zero (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
-have b * a - c * a = 0, by simp [h],
-have (b - c) * a = 0, by rw [mul_sub_right_distrib, this],
-have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha,
-eq_of_sub_eq_zero this
+eq_of_mul_eq_mul_right ha h
 
 /-- Left multiplication by a nonzero element of an integral domain is injective. -/
 theorem eq_of_mul_eq_mul_left_of_ne_zero (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
-have a * b - a * c = 0, by simp [h],
-have a * (b - c) = 0, by rw [mul_sub_left_distrib, this],
-have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha,
-eq_of_sub_eq_zero this
+eq_of_mul_eq_mul_left ha h
 
 /-- Given two elements b, c of an integral domain and a nonzero element a, a*b divides a*c iff
   b divides c. -/

src/data/nat/basic.lean

@@ -27,8 +27,7 @@ instance : canonically_ordered_comm_semiring ℕ :=
   ⟨assume h, let ⟨c, hc⟩ := nat.le.dest h in ⟨c, hc.symm⟩,
     assume ⟨c, hc⟩, hc.symm ▸ nat.le_add_right _ _⟩,
   zero_ne_one       := ne_of_lt zero_lt_one,
-  mul_eq_zero_iff   := assume a b,
-    iff.intro nat.eq_zero_of_mul_eq_zero (by simp [or_imp_distrib] {contextual := tt}),
+  eq_zero_or_eq_zero_of_mul_eq_zero   := assume a b, nat.eq_zero_of_mul_eq_zero,
   bot               := 0,
   bot_le            := nat.zero_le,
   .. (infer_instance : ordered_add_comm_monoid ℕ),