From f92fd0d19459ca991f3090b4ced2e931fc7deceb Mon Sep 17 00:00:00 2001
From: Aaron Anderson <awainverse@gmail.com>
Date: Tue, 11 Aug 2020 09:57:43 +0000
Subject: [PATCH] refactor(algebra/divisibility, associated): generalize
 instances in divisibility, associated (#3714)

generalizes the divisibility relation to noncommutative monoids
adds missing headers to algebra/divisibility
generalizes the instances in many of the lemmas in algebra/associated
reunites (some of the) divisibility API for ordinals with general monoids



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
---
 src/algebra/associated.lean                   | 127 ++++++-------
 src/algebra/divisibility.lean                 | 176 +++++++++++++++---
 src/algebra/gcd_domain.lean                   |  16 +-
 src/algebra/group_power.lean                  |  11 +-
 src/algebra/group_with_zero.lean              |   2 +
 src/algebra/ring/basic.lean                   |  72 +------
 src/analysis/normed_space/basic.lean          |   2 +-
 src/data/equiv/ring.lean                      |   2 +-
 src/data/polynomial/algebra_map.lean          |   3 +-
 src/data/polynomial/field_division.lean       |   2 +-
 src/data/polynomial/ring_division.lean        |   2 +-
 src/field_theory/separable.lean               |   2 +-
 src/number_theory/quadratic_reciprocity.lean  |   2 +-
 src/ring_theory/ideal/basic.lean              |   2 +-
 src/ring_theory/multiplicity.lean             |   3 +-
 src/ring_theory/polynomial/rational_root.lean |   2 +-
 src/ring_theory/power_series.lean             |   2 +-
 src/ring_theory/principal_ideal_domain.lean   |   2 +-
 .../unique_factorization_domain.lean          |   6 +-
 src/set_theory/ordinal_arithmetic.lean        |  18 +-
 src/set_theory/ordinal_notation.lean          |   8 +-
 21 files changed, 246 insertions(+), 216 deletions(-)

diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
index b593e0cf410cf..1fd1dace14b0c 100644
--- a/src/algebra/associated.lean
+++ b/src/algebra/associated.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
 import data.multiset.basic
+import algebra.divisibility
 
 /-!
 # Associated, prime, and irreducible elements.
@@ -14,28 +15,15 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 
-theorem is_unit_iff_dvd_one [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
+theorem is_unit_iff_dvd_one [comm_monoid α] {x : α} : is_unit x ↔ x ∣ 1 :=
 ⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
  λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
 
-theorem is_unit_iff_forall_dvd [comm_semiring α] {x : α} :
+theorem is_unit_iff_forall_dvd [comm_monoid α] {x : α} :
   is_unit x ↔ ∀ y, x ∣ y :=
 is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
 
-theorem mul_dvd_of_is_unit_left [comm_semiring α] {x y z : α} (h : is_unit x) : x * y ∣ z ↔ y ∣ z :=
-⟨dvd_trans (dvd_mul_left _ _),
- dvd_trans $ by simpa using mul_dvd_mul_right (is_unit_iff_dvd_one.1 h) y⟩
-
-theorem mul_dvd_of_is_unit_right [comm_semiring α] {x y z : α} (h : is_unit y) : x * y ∣ z ↔ x ∣ z :=
-by rw [mul_comm, mul_dvd_of_is_unit_left h]
-
-@[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
-mul_dvd_of_is_unit_left (is_unit_unit _)
-
-lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
-units.coe_mul_dvd _ _ _
-
-theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
+theorem is_unit_of_dvd_unit {α} [comm_monoid α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
 
@@ -43,7 +31,7 @@ theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
 ⟨begin rintro ⟨u, rfl⟩, exact (int.units_eq_one_or u).elim (by simp) (by simp) end,
   λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
 
-lemma is_unit_of_dvd_one [comm_semiring α] : ∀a ∣ 1, is_unit (a:α)
+lemma is_unit_of_dvd_one [comm_monoid α] : ∀a ∣ 1, is_unit (a:α)
 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
 
 lemma dvd_and_not_dvd_iff [integral_domain α] {x y : α} :
@@ -58,29 +46,33 @@ lemma pow_dvd_pow_iff [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (
 begin
   split,
   { intro h, rw [← not_lt], intro hmn, apply h1,
-    have : x * x ^ m ∣ 1 * x ^ m,
-    { rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
-    rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
+    have : x ^ m * x ∣ x ^ m * 1,
+    { rw [← pow_succ', mul_one], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
+    rwa [mul_dvd_mul_iff_left, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
   { apply pow_dvd_pow }
 end
 
-/-- prime element of a semiring -/
-def prime [comm_semiring α] (p : α) : Prop :=
+section prime
+variables [comm_monoid_with_zero α]
+
+/-- prime element of a `comm_monoid_with_zero` -/
+def prime (p : α) : Prop :=
 p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
 
 namespace prime
+variables {p : α} (hp : prime p)
 
-lemma ne_zero [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 :=
+lemma ne_zero (hp : prime p) : p ≠ 0 :=
 hp.1
 
-lemma not_unit [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p :=
+lemma not_unit (hp : prime p) : ¬ is_unit p :=
 hp.2.1
 
-lemma div_or_div [comm_semiring α] {p : α} (hp : prime p) {a b : α} (h : p ∣ a * b) :
+lemma div_or_div (hp : prime p) {a b : α} (h : p ∣ a * b) :
   p ∣ a ∨ p ∣ b :=
 hp.2.2 a b h
 
-lemma dvd_of_dvd_pow [comm_semiring α] {p : α} (hp : prime p) {a : α} {n : ℕ} (h : p ∣ a^n) :
+lemma dvd_of_dvd_pow (hp : prime p) {a : α} {n : ℕ} (h : p ∣ a^n) :
   p ∣ a :=
 begin
   induction n with n ih,
@@ -96,13 +88,13 @@ end
 
 end prime
 
-@[simp] lemma not_prime_zero [comm_semiring α] : ¬ prime (0 : α) :=
+@[simp] lemma not_prime_zero : ¬ prime (0 : α) :=
 λ h, h.ne_zero rfl
 
-@[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
+@[simp] lemma not_prime_one : ¬ prime (1 : α) :=
 λ h, h.not_unit is_unit_one
 
-lemma exists_mem_multiset_dvd_of_prime [comm_semiring α] {s : multiset α} {p : α} (hp : prime p) :
+lemma exists_mem_multiset_dvd_of_prime {s : multiset α} {p : α} (hp : prime p) :
   p ∣ s.prod → ∃a∈s, p ∣ a :=
 multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
 assume a s ih h,
@@ -112,6 +104,8 @@ assume a s ih h,
   | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
   end
 
+end prime
+
 /-- `irreducible p` states that `p` is non-unit and only factors into units.
 
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
@@ -134,11 +128,11 @@ end irreducible
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
 by simp [irreducible]
 
-@[simp] theorem not_irreducible_zero [semiring α] : ¬ irreducible (0 : α)
+@[simp] theorem not_irreducible_zero [monoid_with_zero α] : ¬ irreducible (0 : α)
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0
 
-theorem irreducible.ne_zero [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
+theorem irreducible.ne_zero [monoid_with_zero α] : ∀ {p:α}, irreducible p → p ≠ 0
 | _ hp rfl := not_irreducible_zero hp
 
 theorem of_irreducible_mul {α} [monoid α] {x y : α} :
@@ -179,17 +173,15 @@ have hpd : p ∣ x * y, from ⟨z, by rwa [mul_right_inj' hp0] at h⟩,
   (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
 /-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`. -/
-lemma dvd_symm_of_irreducible [comm_semiring α] {p q : α}
+lemma dvd_symm_of_irreducible [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q → q ∣ p :=
 begin
   tactic.unfreeze_local_instances,
   rintros ⟨q', rfl⟩,
-  exact is_unit.mul_right_dvd_of_dvd
-    (or.resolve_left (of_irreducible_mul hq) hp.not_unit)
-    (dvd_refl p)
+  rw is_unit.mul_right_dvd (or.resolve_left (of_irreducible_mul hq) hp.not_unit),
 end
 
-lemma dvd_symm_iff_of_irreducible [comm_semiring α] {p q : α}
+lemma dvd_symm_iff_of_irreducible [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q ↔ q ∣ p :=
 ⟨dvd_symm_of_irreducible hp hq, dvd_symm_of_irreducible hq hp⟩
 
@@ -239,25 +231,28 @@ lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
   a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
 
-lemma dvd_of_associated [comm_ring α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
+lemma dvd_of_associated [monoid α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
 
-lemma dvd_dvd_of_associated [comm_ring α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
+lemma dvd_dvd_of_associated [monoid α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
 ⟨dvd_of_associated h, dvd_of_associated h.symm⟩
 
-theorem associated_of_dvd_dvd [integral_domain α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
+theorem associated_of_dvd_dvd [cancel_monoid_with_zero α]
+  {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
 begin
-  haveI := classical.dec_eq α,
   rcases hab with ⟨c, rfl⟩,
   rcases hba with ⟨d, a_eq⟩,
   by_cases ha0 : a = 0,
   { simp [*] at * },
-  have : a * 1 = a * (c * d),
-  { simpa [mul_assoc] using a_eq },
-  have : 1 = (c * d), from mul_left_cancel' ha0 this,
-  exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
+  have hac0 : a * c ≠ 0,
+  { intro con, rw [con, zero_mul] at a_eq, apply ha0 a_eq, },
+  have : a * (c * d) =  a * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
+  have hcd : (c * d) = 1, from mul_left_cancel' ha0 this,
+  have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
+  have hdc : d * c = 1, from mul_left_cancel' hac0 this,
+  exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
 end
 
-theorem dvd_dvd_iff_associated [integral_domain α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
+theorem dvd_dvd_iff_associated [cancel_monoid_with_zero α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
 ⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, dvd_dvd_of_associated⟩
 
 lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
@@ -275,14 +270,11 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
   end)
 
-lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
-let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
-
-lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
-units.dvd_coe_mul _ _ _
+lemma dvd_iff_dvd_of_rel_left [comm_monoid_with_zero α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
+let ⟨u, hu⟩ := h in hu ▸ units.mul_right_dvd.symm
 
 lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
-let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm
+let ⟨u, hu⟩ := h in hu ▸ units.dvd_mul_right.symm
 
 lemma eq_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
 ⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
@@ -295,7 +287,7 @@ lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : pri
 ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
     ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
-      hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
+      hu ▸ by { simp [units.mul_right_dvd], intros a b, exact hp.div_or_div }⟩⟩
 
 lemma prime_iff_of_associated [comm_semiring α] {p q : α}
   (h : p ~ᵤ q) : prime p ↔ prime q :=
@@ -386,11 +378,9 @@ instance : comm_monoid (associates α) :=
     assume a b, show ⟦a * b⟧ = ⟦b * a⟧, by rw [mul_comm] }
 
 instance : preorder (associates α) :=
-{ le := λa b, ∃c, a * c = b,
-  le_refl := assume a, ⟨1, by simp⟩,
-  le_trans := assume a b c ⟨f₁, h₁⟩ ⟨f₂, h₂⟩, ⟨f₁ * f₂, h₂ ▸ h₁ ▸ (mul_assoc _ _ _).symm⟩}
-
-instance : has_dvd (associates α) := ⟨(≤)⟩
+{ le := has_dvd.dvd,
+  le_refl := dvd_refl,
+  le_trans := λ a b c, dvd_trans}
 
 @[simp] lemma mk_one : associates.mk (1 : α) = 1 := rfl
 
@@ -439,10 +429,10 @@ section order
 theorem mul_mono {a b c d : associates α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
   a * c ≤ b * d :=
 let ⟨x, hx⟩ := h₁, ⟨y, hy⟩ := h₂ in
-⟨x * y, by simp [hx.symm, hy.symm, mul_comm, mul_assoc, mul_left_comm]⟩
+⟨x * y, by simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]⟩
 
 theorem one_le {a : associates α} : 1 ≤ a :=
-⟨a, one_mul a⟩
+dvd.intro _ (one_mul a)
 
 theorem prod_le_prod {p q : multiset (associates α)} (h : p ≤ q) : p.prod ≤ q.prod :=
 begin
@@ -493,9 +483,9 @@ variables [comm_semiring α]
 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,
     let ⟨d, hd⟩ := (quotient.exact hc).symm in
-    ⟨(↑d⁻¹) * c,
-      calc b = (a * c) * ↑d⁻¹ : by rw [← hd, mul_assoc, units.mul_inv, mul_one]
-        ... = a * (↑d⁻¹ * c) : by ac_refl⟩) hc'
+    ⟨(↑d) * c,
+      calc b = (a * c) * ↑d : hd.symm
+        ... = a * (↑d * c) : by ac_refl⟩) hc'
 
 theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → associates.mk a ≤ associates.mk b :=
 assume ⟨c, hc⟩, ⟨associates.mk c, by simp [hc]; refl⟩
@@ -518,7 +508,7 @@ hp.2.2 a b h
 lemma exists_mem_multiset_le_of_prime {s : multiset (associates α)} {p : associates α}
   (hp : prime p) :
   p ≤ s.prod → ∃a∈s, p ≤ a :=
-multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq).1).elim) $
+multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq.symm).1).elim) $
 assume a s ih h,
   have p ≤ a * s.prod, by simpa using h,
   match hp.le_or_le this with
@@ -549,13 +539,8 @@ section integral_domain
 variable [integral_domain α]
 
 instance : partial_order (associates α) :=
-{ le_antisymm := assume a' b',
-    quotient.induction_on₂ a' b' $ assume a b ⟨f₁', h₁⟩ ⟨f₂', h₂⟩,
-    (quotient.induction_on₂ f₁' f₂' $ assume f₁ f₂ h₁ h₂,
-      let ⟨c₁, h₁⟩ := quotient.exact h₁, ⟨c₂, h₂⟩ := quotient.exact h₂ in
-      quotient.sound $ associated_of_dvd_dvd
-        (h₁ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
-        (h₂ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)) h₁ h₂
+{ le_antisymm := λ a' b', quotient.induction_on₂ a' b' (λ a b hab hba,
+  quot.sound $ associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba))
   .. associates.preorder }
 
 instance : order_bot (associates α) :=
@@ -565,7 +550,7 @@ instance : order_bot (associates α) :=
 
 instance : order_top (associates α) :=
 { top := 0,
-  le_top := assume a, ⟨0, mul_zero a⟩,
+  le_top := assume a, ⟨0, (mul_zero a).symm⟩,
   .. associates.partial_order }
 
 instance : no_zero_divisors (associates α) :=
diff --git a/src/algebra/divisibility.lean b/src/algebra/divisibility.lean
index 2db55685ca078..43a6673506817 100644
--- a/src/algebra/divisibility.lean
+++ b/src/algebra/divisibility.lean
@@ -1,13 +1,44 @@
+/-
+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, Amelia Livingston, Yury Kudryashov,
+Neil Strickland, Aaron Anderson
+-/
+
 import algebra.group_with_zero
 
+/-!
+# Divisibility
+
+This file defines the basics of the divisibility relation in the context of `(comm_)` `monoid`s
+`(_with_zero)`.
+
+## Main definitions
+
+ * `monoid.has_dvd`
+
+## Implementation notes
+
+The divisibility relation is defined for all monoids, and as such, depends on the order of
+  multiplication if the monoid is not commutative. There are two possible conventions for
+  divisibility in the noncommutative context, and this relation follows the convention for ordinals,
+  so `a | b` is defined as `∃ c, b = a * c`.
+
+## Tags
+
+divisibility, divides
+-/
+
 variables {α : Type*}
 
-section comm_monoid
+section monoid
 
-variables [comm_monoid α] {a b c : α}
+variables [monoid α] {a b c : α}
 
+/-- There are two possible conventions for divisibility, which coincide in a `comm_monoid`.
+    This matches the convention for ordinals. -/
 @[priority 100]
-instance comm_monoid_has_dvd : has_dvd α :=
+instance monoid_has_dvd : has_dvd α :=
 has_dvd.mk (λ a b, ∃ c, b = a * c)
 
 -- TODO: this used to not have c explicit, but that seems to be important
@@ -17,22 +48,11 @@ exists.intro c h^.symm
 
 alias dvd.intro ← dvd_of_mul_right_eq
 
-theorem dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
-dvd.intro _ (begin rewrite mul_comm at h, apply h end)
-
-alias dvd.intro_left ← dvd_of_mul_left_eq
-
 theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c := h
 
 theorem dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
 exists.elim H₁ H₂
 
-theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
-dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
-
-theorem dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
-exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
-
 @[refl, simp] theorem dvd_refl (a : α) : a ∣ a :=
 dvd.intro 1 (by simp)
 
@@ -46,18 +66,40 @@ end
 
 alias dvd_trans ← dvd.trans
 
-@[simp] theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (by simp)
+theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (by simp)
 
 @[simp] theorem dvd_mul_right (a b : α) : a ∣ a * b := dvd.intro b rfl
 
-@[simp] theorem dvd_mul_left (a b : α) : a ∣ b * a := dvd.intro b (by simp)
-
 theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
 dvd.elim h (λ d h', begin rw [h', mul_assoc], apply dvd_mul_right end)
 
+theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
+dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end)
+
+end monoid
+
+section comm_monoid
+
+variables [comm_monoid α] {a b c : α}
+
+theorem dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
+dvd.intro _ (begin rewrite mul_comm at h, apply h end)
+
+alias dvd.intro_left ← dvd_of_mul_left_eq
+
+theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
+dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
+
+theorem dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
+exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
+
+@[simp] theorem dvd_mul_left (a b : α) : a ∣ b * a := dvd.intro b (mul_comm a b)
+
 theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b :=
 begin rw mul_comm, exact dvd_mul_of_dvd_left h _ end
 
+local attribute [simp] mul_assoc mul_comm mul_left_comm
+
 theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
 | a ._ c ._ ⟨e, rfl⟩ ⟨f, rfl⟩ := ⟨e * f, by simp⟩
 
@@ -67,26 +109,110 @@ mul_dvd_mul (dvd_refl a) h
 theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
 mul_dvd_mul h (dvd_refl c)
 
-theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
-dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end)
-
 theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
 dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq]))
 
 end comm_monoid
 
-section comm_monoid_with_zero
+section monoid_with_zero
 
-variables [comm_monoid_with_zero α] {a : α}
+variables [monoid_with_zero α] {a : α}
 
 theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
 dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
 
-/-- Given an element a of a commutative monoid with zero, there exists another element whose product
-    with zero equals a iff a equals zero. -/
+/-- Given an element `a` of a commutative monoid with zero, there exists another element whose
+    product with zero equals `a` iff `a` equals zero. -/
 @[simp] lemma zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
 ⟨eq_zero_of_zero_dvd, λ h, by rw h⟩
 
 @[simp] theorem dvd_zero (a : α) : a ∣ 0 := dvd.intro 0 (by simp)
 
-end comm_monoid_with_zero
+end monoid_with_zero
+
+/-- Given two elements `b`, `c` of an integral domain and a nonzero element `a`,
+ `a*b` divides `a*c` iff `b` divides `c`. -/
+theorem mul_dvd_mul_iff_left [cancel_monoid_with_zero α] {a b c : α}
+  (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c :=
+exists_congr $ λ d, by rw [mul_assoc, mul_right_inj' ha]
+
+/-!
+### Units in various monoids
+-/
+
+namespace units
+
+section monoid
+variables [monoid α] {a b : α} {u : units α}
+
+/-- Elements of the unit group of a monoid represented as elements of the monoid
+    divide any element of the monoid. -/
+lemma coe_dvd : ↑u ∣ a := ⟨↑u⁻¹ * a, by simp⟩
+
+/-- In a monoid, an element `a` divides an element `b` iff `a` divides all
+    associates of `b`. -/
+lemma dvd_mul_right : a ∣ b * u ↔ a ∣ b :=
+iff.intro
+  (assume ⟨c, eq⟩, ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, units.mul_inv_cancel_right]⟩)
+  (assume ⟨c, eq⟩, eq.symm ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
+
+/-- In a monoid, an element a divides an element b iff all associates of `a` divide `b`.-/
+lemma mul_right_dvd : a * u ∣ b ↔ a ∣ b :=
+iff.intro
+  (λ ⟨c, eq⟩, ⟨↑u * c, eq.trans (mul_assoc _ _ _)⟩)
+  (λ h, dvd_trans (dvd.intro ↑u⁻¹ (by rw [mul_assoc, u.mul_inv, mul_one])) h)
+
+end monoid
+
+section comm_monoid
+variables [comm_monoid α] {a b : α} {u : units α}
+
+/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
+    associates of `b`. -/
+lemma dvd_mul_left : a ∣ u * b ↔ a ∣ b := by { rw mul_comm, apply dvd_mul_right }
+
+/-- In a commutative monoid, an element `a` divides an element `b` iff all
+  left associates of `a` divide `b`.-/
+lemma mul_left_dvd : ↑u * a ∣ b ↔ a ∣ b :=
+by { rw mul_comm, apply mul_right_dvd }
+
+end comm_monoid
+
+end units
+
+namespace is_unit
+
+section monoid
+
+variables [monoid α] {a b u : α} (hu : is_unit u)
+include hu
+
+/-- Units of a monoid divide any element of the monoid. -/
+@[simp] lemma dvd : u ∣ a := by { rcases hu with ⟨u, rfl⟩, apply units.coe_dvd, }
+
+@[simp] lemma dvd_mul_right : a ∣ b * u ↔ a ∣ b :=
+by { rcases hu with ⟨u, rfl⟩, apply units.dvd_mul_right, }
+
+/-- In a monoid, an element a divides an element b iff all associates of `a` divide `b`.-/
+@[simp] lemma mul_right_dvd : a * u ∣ b ↔ a ∣ b :=
+by { rcases hu with ⟨u, rfl⟩, apply units.mul_right_dvd, }
+
+end monoid
+
+section comm_monoid
+variables [comm_monoid α] (a b u : α) (hu : is_unit u)
+include hu
+
+/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
+    associates of `b`. -/
+@[simp] lemma dvd_mul_left : a ∣ u * b ↔ a ∣ b :=
+by { rcases hu with ⟨u, rfl⟩, apply units.dvd_mul_left, }
+
+/-- In a commutative monoid, an element `a` divides an element `b` iff all
+  left associates of `a` divide `b`.-/
+@[simp] lemma mul_left_dvd : u * a ∣ b ↔ a ∣ b :=
+by { rcases hu with ⟨u, rfl⟩, apply units.mul_left_dvd, }
+
+end comm_monoid
+
+end is_unit
diff --git a/src/algebra/gcd_domain.lean b/src/algebra/gcd_domain.lean
index 2ad4bb211c1be..0533c298cd81f 100644
--- a/src/algebra/gcd_domain.lean
+++ b/src/algebra/gcd_domain.lean
@@ -68,7 +68,7 @@ lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
 
 theorem norm_unit_mul_norm_unit (a : α) : norm_unit (a * norm_unit a) = 1 :=
 classical.by_cases (assume : a = 0, by simp only [this, norm_unit_zero, zero_mul]) $
-  assume h, by rw [norm_unit_mul h (units.coe_ne_zero _), norm_unit_coe_units, mul_inv_eq_one]
+  assume h, by rw [norm_unit_mul h (units.ne_zero _), norm_unit_coe_units, mul_inv_eq_one]
 
 theorem normalize_idem (x : α) : normalize (normalize x) = normalize x :=
 by rw [normalize, normalize, norm_unit_mul_norm_unit, units.coe_one, mul_one]
@@ -79,14 +79,14 @@ begin
   rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩,
   refine classical.by_cases (by rintro rfl; simp only [zero_mul]) (assume ha : a ≠ 0, _),
   suffices : a * ↑(norm_unit a) = a * ↑u * ↑(norm_unit a) * ↑u⁻¹,
-    by simpa only [normalize, mul_assoc, norm_unit_mul ha u.coe_ne_zero, norm_unit_coe_units],
+    by simpa only [normalize, mul_assoc, norm_unit_mul ha u.ne_zero, norm_unit_coe_units],
   calc a * ↑(norm_unit a) = a * ↑(norm_unit a) * ↑u * ↑u⁻¹:
       (units.mul_inv_cancel_right _ _).symm
     ... = a * ↑u * ↑(norm_unit a) * ↑u⁻¹ : by rw mul_right_comm a
 end
 
 lemma normalize_eq_normalize_iff {x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x :=
-⟨λ h, ⟨dvd_mul_unit_iff.1 ⟨_, h.symm⟩, dvd_mul_unit_iff.1 ⟨_, h⟩⟩,
+⟨λ h, ⟨units.dvd_mul_right.1 ⟨_, h.symm⟩, units.dvd_mul_right.1 ⟨_, h⟩⟩,
 λ ⟨hxy, hyx⟩, normalize_eq_normalize hxy hyx⟩
 
 theorem dvd_antisymm_of_normalize_eq {a b : α}
@@ -95,10 +95,10 @@ theorem dvd_antisymm_of_normalize_eq {a b : α}
 ha ▸ hb ▸ normalize_eq_normalize hab hba
 
 @[simp] lemma dvd_normalize_iff {a b : α} : a ∣ normalize b ↔ a ∣ b :=
-dvd_mul_unit_iff
+units.dvd_mul_right
 
 @[simp] lemma normalize_dvd_iff {a b : α} : normalize a ∣ b ↔ a ∣ b :=
-mul_unit_dvd_iff
+units.mul_right_dvd
 
 end normalization_domain
 
@@ -109,7 +109,7 @@ local attribute [instance] associated.setoid
 
 protected def out : associates α → α :=
 quotient.lift (normalize : α → α) $ λ a b ⟨u, hu⟩, hu ▸
-normalize_eq_normalize ⟨_, rfl⟩ (mul_unit_dvd_iff.2 $ dvd_refl a)
+normalize_eq_normalize ⟨_, rfl⟩ (units.mul_right_dvd.2 $ dvd_refl a)
 
 lemma out_mk (a : α) : (associates.mk a).out = normalize a := rfl
 
@@ -282,7 +282,7 @@ iff.intro
   (assume h : lcm a b = 0,
     have normalize (a * b) = 0,
       by rw [← gcd_mul_lcm _ _, h, mul_zero],
-    by simpa only [normalize_eq_zero, mul_eq_zero, units.coe_ne_zero, or_false])
+    by simpa only [normalize_eq_zero, mul_eq_zero, units.ne_zero, or_false])
   (by rintro (rfl | rfl); [apply lcm_zero_left, apply lcm_zero_right])
 
 @[simp] lemma normalize_lcm (a b : α) : normalize (lcm a b) = lcm a b :=
@@ -319,7 +319,7 @@ theorem lcm_dvd_lcm {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣
 lcm_dvd (dvd.trans hab (dvd_lcm_left _ _)) (dvd.trans hcd (dvd_lcm_right _ _))
 
 @[simp] theorem lcm_units_coe_left (u : units α) (a : α) : lcm ↑u a = normalize a :=
-lcm_eq_normalize (lcm_dvd (units.coe_dvd _ _) (dvd_refl _)) (dvd_lcm_right _ _)
+lcm_eq_normalize (lcm_dvd units.coe_dvd (dvd_refl _)) (dvd_lcm_right _ _)
 
 @[simp] theorem lcm_units_coe_right (a : α) (u : units α) : lcm a ↑u = normalize a :=
 (lcm_comm a u).trans $ lcm_units_coe_left _ _
diff --git a/src/algebra/group_power.lean b/src/algebra/group_power.lean
index dab20bacc571d..a608bb4307b46 100644
--- a/src/algebra/group_power.lean
+++ b/src/algebra/group_power.lean
@@ -437,7 +437,7 @@ by rw [nsmul_eq_mul', nsmul_eq_mul', mul_assoc]
 theorem mul_nsmul_assoc [semiring R] (a b : R) (n : ℕ) : n •ℕ (a * b) = n •ℕ a * b :=
 by rw [nsmul_eq_mul, nsmul_eq_mul, mul_assoc]
 
-lemma zero_pow [semiring R] : ∀ {n : ℕ}, 0 < n → (0 : R) ^ n = 0
+lemma zero_pow [monoid_with_zero R] : ∀ {n : ℕ}, 0 < n → (0 : R) ^ n = 0
 | (n+1) _ := zero_mul _
 
 @[simp, norm_cast] theorem nat.cast_pow [semiring R] (n m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
@@ -465,10 +465,10 @@ theorem neg_one_pow_eq_or [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n
   (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
   (λ h, by rw [pow_succ, h, mul_one])
 
-lemma pow_dvd_pow [comm_semiring R] (a : R) {m n : ℕ} (h : m ≤ n) :
+lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :
   a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_sub_cancel' h]⟩
 
-theorem pow_dvd_pow_of_dvd [comm_semiring R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
+theorem pow_dvd_pow_of_dvd [comm_monoid R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
 | 0     := dvd_refl _
 | (n+1) := mul_dvd_mul h (pow_dvd_pow_of_dvd n)
 
@@ -524,7 +524,7 @@ by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
 theorem sq_sub_sq [comm_ring R] (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
 by rw [pow_two, pow_two, mul_self_sub_mul_self]
 
-theorem pow_eq_zero [domain R] {x : R} {n : ℕ} (H : x^n = 0) : x = 0 :=
+theorem pow_eq_zero [monoid_with_zero R] [no_zero_divisors R] {x : R} {n : ℕ} (H : x^n = 0) : x = 0 :=
 begin
   induction n with n ih,
   { rw pow_zero at H,
@@ -532,7 +532,8 @@ begin
   exact or.cases_on (mul_eq_zero.1 H) id ih
 end
 
-@[field_simps] theorem pow_ne_zero [domain R] {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
+@[field_simps] theorem pow_ne_zero [monoid_with_zero R] [no_zero_divisors R]
+  {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 mt pow_eq_zero h
 
 theorem nsmul_nonneg [ordered_add_comm_monoid R] {a : R} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n •ℕ a
diff --git a/src/algebra/group_with_zero.lean b/src/algebra/group_with_zero.lean
index 2c13d011d9c6c..d0ad1b53313f4 100644
--- a/src/algebra/group_with_zero.lean
+++ b/src/algebra/group_with_zero.lean
@@ -272,6 +272,8 @@ variables [monoid_with_zero M₀]
 
 namespace units
 
+/-- An element of the unit group of a nonzero monoid with zero represented as an element
+    of the monoid is nonzero. -/
 @[simp] lemma ne_zero [nontrivial M₀] (u : units M₀) :
   (u : M₀) ≠ 0 :=
 left_ne_zero_of_mul_eq_one u.mul_inv
diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean
index 4fb1bcfa70b65..4b8a9d7d72007 100644
--- a/src/algebra/ring/basic.lean
+++ b/src/algebra/ring/basic.lean
@@ -618,7 +618,7 @@ theorem dvd_add_iff_left (h : a ∣ c) : a ∣ b ↔ a ∣ b + c :=
 theorem dvd_add_iff_right (h : a ∣ b) : a ∣ c ↔ a ∣ b + c :=
 by rw add_comm; exact dvd_add_iff_left h
 
-theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right two_dvd_bit0).symm
+theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@two_dvd_bit0 _ _ a)).symm
 
 /-- Representation of a difference of two squares in a commutative ring as a product. -/
 theorem mul_self_sub_mul_self (a b : α) : a * a - b * b = (a + b) * (a - b) :=
@@ -692,11 +692,6 @@ lemma succ_ne_self [ring α] [nontrivial α] (a : α) : a + 1 ≠ a :=
 lemma pred_ne_self [ring α] [nontrivial α] (a : α) : a - 1 ≠ a :=
 λ h, one_ne_zero (neg_injective ((add_right_inj a).mp (by { convert h, simp })))
 
-/-- An element of the unit group of a nonzero semiring represented as an element
-    of the semiring is nonzero. -/
-lemma units.coe_ne_zero [semiring α] [nontrivial α] (u : units α) : (u : α) ≠ 0 :=
-λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3
-
 /-- 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. -/
@@ -752,11 +747,6 @@ by rw [← sub_eq_zero, mul_self_sub_mul_self, mul_eq_zero, or_comm, sub_eq_zero
 lemma mul_self_eq_one_iff {a : α} : a * a = 1 ↔ a = 1 ∨ a = -1 :=
 by rw [← mul_self_eq_mul_self_iff, one_mul]
 
-/-- Given two elements b, c of an integral domain and a nonzero element a, a*b divides a*c iff
-  b divides c. -/
-theorem mul_dvd_mul_iff_left (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c :=
-exists_congr $ λ d, by rw [mul_assoc, mul_right_inj' ha]
-
 /-- Given two elements a, b of an integral domain and a nonzero element c, a*c divides b*c iff
   a divides b. -/
 theorem mul_dvd_mul_iff_right (hc : c ≠ 0) : a * c ∣ b * c ↔ a ∣ b :=
@@ -769,66 +759,6 @@ by { rw inv_eq_iff_mul_eq_one, simp only [units.ext_iff], push_cast, exact mul_s
 
 end integral_domain
 
-/-!
-### Units in various rings
--/
-
-namespace units
-
-section comm_semiring
-variables [comm_semiring α] (a b : α) (u : units α)
-
-/-- Elements of the unit group of a commutative semiring represented as elements of the semiring
-    divide any element of the semiring. -/
-@[simp] lemma coe_dvd : ↑u ∣ a := ⟨↑u⁻¹ * a, by simp⟩
-
-/-- In a commutative semiring, an element a divides an element b iff a divides all
-    associates of b. -/
-@[simp] lemma dvd_coe_mul : a ∣ b * u ↔ a ∣ b :=
-iff.intro
-  (assume ⟨c, eq⟩, ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, units.mul_inv_cancel_right]⟩)
-  (assume ⟨c, eq⟩, eq.symm ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
-
-/-- An element of a commutative semiring divides a unit iff the element divides one. -/
-@[simp] lemma dvd_coe : a ∣ ↑u ↔ a ∣ 1 :=
-suffices a ∣ 1 * ↑u ↔ a ∣ 1, by simpa,
-dvd_coe_mul _ _ _
-
-/-- In a commutative semiring, an element a divides an element b iff all associates of a divide b.-/
-@[simp] lemma coe_mul_dvd : a * u ∣ b ↔ a ∣ b :=
-iff.intro
-  (assume ⟨c, eq⟩, ⟨c * ↑u, eq.symm ▸ by ac_refl⟩)
-  (assume h, suffices a * ↑u ∣ b * 1, by simpa, mul_dvd_mul h (coe_dvd _ _))
-
-end comm_semiring
-
-end units
-
-namespace is_unit
-
-section comm_semiring
-variables [comm_semiring R]
-
-lemma mul_right_dvd_of_dvd {a b c : R} (hb : is_unit b) (h : a ∣ c) : a * b ∣ c :=
-begin
-  rcases hb with ⟨b, rfl⟩,
-  rcases h with ⟨c', rfl⟩,
-  use (b⁻¹ : units R) * c',
-  rw [mul_assoc, units.mul_inv_cancel_left]
-end
-
-lemma mul_left_dvd_of_dvd {a b c : R} (hb : is_unit b) (h : a ∣ c) : b * a ∣ c :=
-begin
-  rcases hb with ⟨b, rfl⟩,
-  rcases h with ⟨c', rfl⟩,
-  use (b⁻¹ : units R) * c',
-  rw [mul_comm (b : R) a, mul_assoc, units.mul_inv_cancel_left]
-end
-
-end comm_semiring
-
-end is_unit
-
 namespace ring
 variables [ring R]
 open_locale classical
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 2fd91ca856cee..c9961ab3be056 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -456,7 +456,7 @@ begin
 end
 
 lemma units.norm_pos {α : Type*} [normed_ring α] [nontrivial α] (x : units α) : 0 < ∥(x:α)∥ :=
-norm_pos_iff.mpr (units.coe_ne_zero x)
+norm_pos_iff.mpr (units.ne_zero x)
 
 /-- In a normed ring, the left-multiplication `add_monoid_hom` is bounded. -/
 lemma mul_left_bound {α : Type*} [normed_ring α] (x : α) :
diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
index 6fc2d3a91ff81..80c9da149066c 100644
--- a/src/data/equiv/ring.lean
+++ b/src/data/equiv/ring.lean
@@ -287,7 +287,7 @@ namespace equiv
 variables (K : Type*) [division_ring K]
 
 def units_equiv_ne_zero : units K ≃ {a : K | a ≠ 0} :=
-⟨λ a, ⟨a.1, a.coe_ne_zero⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩
+⟨λ a, ⟨a.1, a.ne_zero⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩
 
 variable {K}
 
diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean
index 34f3458c6de25..08d08bb3ab3f7 100644
--- a/src/data/polynomial/algebra_map.lean
+++ b/src/data/polynomial/algebra_map.lean
@@ -168,7 +168,8 @@ begin
   by_cases hi : i ∈ f.support,
   { unfold polynomial.eval polynomial.eval₂ finsupp.sum id at dvd_eval,
     rw [←finset.insert_erase hi, finset.sum_insert (finset.not_mem_erase _ _)] at dvd_eval,
-    refine (dvd_add_left (finset.dvd_sum _)).mp dvd_eval,
+    refine (dvd_add_left _).mp dvd_eval,
+    apply finset.dvd_sum,
     intros j hj,
     exact dvd_terms j (finset.ne_of_mem_erase hj) },
   { convert dvd_zero p,
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index 416ce682af36a..66f70fa7906ab 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -248,7 +248,7 @@ instance : normalization_domain (polynomial R) :=
     have hu : degree ↑u⁻¹ = 0, from degree_eq_zero_of_is_unit ⟨u⁻¹, rfl⟩,
     begin
       apply units.ext,
-      rw [dif_neg (units.coe_ne_zero u)],
+      rw [dif_neg (units.ne_zero u)],
       conv_rhs {rw eq_C_of_degree_eq_zero hu},
       refine C_inj.2 _,
       rw [← nat_degree_eq_of_degree_eq_some hu, leading_coeff,
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index f1a35669250b9..0d4e17f6b75e7 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -301,7 +301,7 @@ lemma coeff_coe_units_zero_ne_zero (u : units (polynomial R)) :
 begin
   conv in (0) {rw [← nat_degree_coe_units u]},
   rw [← leading_coeff, ne.def, leading_coeff_eq_zero],
-  exact units.coe_ne_zero _
+  exact units.ne_zero _
 end
 
 lemma degree_eq_degree_of_associated (h : associated p q) : degree p = degree q :=
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index d14451cb4ab12..24e4f2fc822eb 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -253,7 +253,7 @@ theorem separable_iff_derivative_ne_zero {f : polynomial F} (hf : irreducible f)
 ⟨λ h1 h2, hf.1 $ is_coprime_zero_right.1 $ h2 ▸ h1,
 λ h, is_coprime_of_dvd (mt and.right h) $ λ g hg1 hg2 ⟨p, hg3⟩ hg4,
 let ⟨u, hu⟩ := (hf.2 _ _ hg3).resolve_left hg1 in
-have f ∣ f.derivative, by { conv_lhs { rw [hg3, ← hu] }, rwa mul_unit_dvd_iff },
+have f ∣ f.derivative, by { conv_lhs { rw [hg3, ← hu] }, rwa units.mul_right_dvd },
 not_lt_of_le (nat_degree_le_of_dvd this h) $ nat_degree_derivative_lt h⟩
 
 theorem separable_map (f : F →+* K) {p : polynomial F} : (p.map f).separable ↔ p.separable :=
diff --git a/src/number_theory/quadratic_reciprocity.lean b/src/number_theory/quadratic_reciprocity.lean
index edf24195a3814..83c0d4adb0e16 100644
--- a/src/number_theory/quadratic_reciprocity.lean
+++ b/src/number_theory/quadratic_reciprocity.lean
@@ -131,7 +131,7 @@ begin
     rw [Ico.mem, ← nat.succ_sub hp, nat.succ_sub_one],
     split,
     { apply nat.pos_of_ne_zero, rw ← @val_zero p,
-      assume h, apply units.coe_ne_zero a (val_injective p h) },
+      assume h, apply units.ne_zero a (val_injective p h) },
     { exact val_lt _ } },
   { intros a ha, simp only [cast_id, nat_cast_val], },
   { intros _ _ _ _ h, rw units.ext_iff, exact val_injective p h },
diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean
index 3bf4f403f6d53..55a81b46916a7 100644
--- a/src/ring_theory/ideal/basic.lean
+++ b/src/ring_theory/ideal/basic.lean
@@ -132,7 +132,7 @@ lemma span_singleton_mul_right_unit {a : α} (h2 : is_unit a) (x : α) :
 begin
   apply le_antisymm,
   { rw span_singleton_le_span_singleton, use a},
-  { rw span_singleton_le_span_singleton, rw mul_dvd_of_is_unit_right h2}
+  { rw span_singleton_le_span_singleton, rw is_unit.mul_right_dvd h2}
 end
 
 lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) :
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 7e0b62804d76b..069560e09e96d 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -323,8 +323,7 @@ have hdiv : p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 +
 have hsucc : ¬p ^ ((get (multiplicity p a) ((finite_mul_iff hp).1 h).1 +
     get (multiplicity p b) ((finite_mul_iff hp).1 h).2) + 1) ∣ a * b,
   from λ h, not_or (is_greatest' _ (lt_succ_self _)) (is_greatest' _ (lt_succ_self _))
-    (succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp (by convert hdiva)
-      (by convert hdivb) h),
+    (by exact succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h),
 by rw [← enat.coe_inj, enat.coe_get, eq_some_iff];
   exact ⟨hdiv, hsucc⟩
 
diff --git a/src/ring_theory/polynomial/rational_root.lean b/src/ring_theory/polynomial/rational_root.lean
index 32396354c5e60..8b98cd4454735 100644
--- a/src/ring_theory/polynomial/rational_root.lean
+++ b/src/ring_theory/polynomial/rational_root.lean
@@ -178,7 +178,7 @@ begin
     by_cases hr : f.num r = 0,
     { obtain ⟨u, hu⟩ := is_unit_pow p.nat_degree (f.is_unit_denom_of_num_eq_zero hr),
       rw ←hu at this,
-      exact dvd_mul_unit_iff.mp this },
+      exact units.dvd_mul_right.mp this },
     { refine dvd_of_dvd_mul_left_of_no_prime_factors hr _ this,
       intros q dvd_num dvd_denom_pow hq,
       apply hq.not_unit,
diff --git a/src/ring_theory/power_series.lean b/src/ring_theory/power_series.lean
index fcbc5cdb47e79..b620b41570403 100644
--- a/src/ring_theory/power_series.lean
+++ b/src/ring_theory/power_series.lean
@@ -678,7 +678,7 @@ lemma inv_eq_zero {φ : mv_power_series σ α} :
 @[simp] lemma inv_of_unit_eq' (φ : mv_power_series σ α) (u : units α) (h : constant_coeff σ α φ = u) :
   inv_of_unit φ u = φ⁻¹ :=
 begin
-  rw ← inv_of_unit_eq φ (h.symm ▸ u.coe_ne_zero),
+  rw ← inv_of_unit_eq φ (h.symm ▸ u.ne_zero),
   congr' 1, rw [units.ext_iff], exact h.symm,
 end
 
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
index f37bee1fc2515..18e69fa216de5 100644
--- a/src/ring_theory/principal_ideal_domain.lean
+++ b/src/ring_theory/principal_ideal_domain.lean
@@ -147,7 +147,7 @@ lemma is_maximal_of_irreducible {p : R} (hp : irreducible p) :
   erw ideal.span_singleton_eq_top,
   unfreezingI { rcases ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩ },
   refine (of_irreducible_mul hp).resolve_right (mt (λ hb, _) (not_le_of_lt hI)),
-  erw [ideal.span_singleton_le_span_singleton, mul_dvd_of_is_unit_right hb]
+  erw [ideal.span_singleton_le_span_singleton, is_unit.mul_right_dvd hb]
 end⟩
 
 lemma irreducible_iff_prime {p : R} : irreducible p ↔ prime p :=
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
index c811e2321981d..22d9865b5c54e 100644
--- a/src/ring_theory/unique_factorization_domain.lean
+++ b/src/ring_theory/unique_factorization_domain.lean
@@ -270,10 +270,10 @@ theorem prod_le_prod_iff_le {p q : multiset (associates α)}
   p.prod ≤ q.prod ↔ p ≤ q :=
 iff.intro
   begin
-    rintros ⟨⟨c⟩, eq⟩,
+    rintros ⟨⟨c⟩, eqc⟩,
     have : c ≠ 0, from (mt mk_eq_zero.2 $
       assume (hc : quot.mk setoid.r c = 0),
-      have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 $ eq ▸ hc.symm ▸ mul_zero _,
+      have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 $ eqc.symm ▸ hc.symm ▸ mul_zero _,
       not_irreducible_zero ((irreducible_mk_iff 0).1 $ hq _ this)),
     have : associates.mk (factors c).prod = quot.mk setoid.r c,
       from mk_eq_mk_iff_associated.2 (factors_prod this),
@@ -481,7 +481,7 @@ begin
     exact is_unit_iff_forall_dvd.mp
       (no_factors_of_no_prime_factors ha @no_factors (dvd_refl a) (dvd_zero a)) _ },
   { rintros _ ⟨x, rfl⟩ _ a_dvd_bx,
-    apply dvd_mul_unit_iff.mp a_dvd_bx },
+    apply units.dvd_mul_right.mp a_dvd_bx },
   { intros c p hc hp ih no_factors a_dvd_bpc,
     apply ih (λ q dvd_a dvd_c hq, no_factors dvd_a (dvd_mul_of_dvd_right dvd_c _) hq),
     rw mul_left_comm at a_dvd_bpc,
diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean
index b8b0bfc05ca47..6f1946c93193e 100644
--- a/src/set_theory/ordinal_arithmetic.lean
+++ b/src/set_theory/ordinal_arithmetic.lean
@@ -781,24 +781,10 @@ begin
   rcases h with h|⟨rfl, h⟩, exact add_is_limit a h, simpa only [add_zero]
 end
 
-/-- Divisibility is defined by right multiplication:
-  `a ∣ b` if there exists `c` such that `b = a * c`. -/
-instance : has_dvd ordinal := ⟨λ a b, ∃ c, b = a * c⟩
-
-theorem dvd_def {a b : ordinal} : a ∣ b ↔ ∃ c, b = a * c := iff.rfl
-
-theorem dvd_mul (a b : ordinal) : a ∣ a * b := ⟨_, rfl⟩
-
-theorem dvd_trans : ∀ {a b c : ordinal}, a ∣ b → b ∣ c → a ∣ c
-| a _ _ ⟨b, rfl⟩ ⟨c, rfl⟩ := ⟨b * c, mul_assoc _ _ _⟩
-
-theorem dvd_mul_of_dvd {a b : ordinal} (c) (h : a ∣ b) : a ∣ b * c :=
-dvd_trans h (dvd_mul _ _)
-
 theorem dvd_add_iff : ∀ {a b c : ordinal}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
 | a _ c ⟨b, rfl⟩ :=
  ⟨λ ⟨d, e⟩, ⟨d - b, by rw [mul_sub, ← e, add_sub_cancel]⟩,
-  λ ⟨d, e⟩, by rw [e, ← mul_add]; apply dvd_mul⟩
+  λ ⟨d, e⟩, by { rw [e, ← mul_add], apply dvd_mul_right }⟩
 
 theorem dvd_add {a b c : ordinal} (h₁ : a ∣ b) : a ∣ c → a ∣ b + c :=
 (dvd_add_iff h₁).2
@@ -1093,7 +1079,7 @@ end
 
 theorem power_dvd_power (a) {b c : ordinal}
   (h : b ≤ c) : a ^ b ∣ a ^ c :=
-by rw [← add_sub_cancel_of_le h, power_add]; apply dvd_mul
+by { rw [← add_sub_cancel_of_le h, power_add], apply dvd_mul_right }
 
 theorem power_dvd_power_iff {a b c : ordinal}
   (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c :=
diff --git a/src/set_theory/ordinal_notation.lean b/src/set_theory/ordinal_notation.lean
index 8301d2dfa349a..d157cdd795915 100644
--- a/src/set_theory/ordinal_notation.lean
+++ b/src/set_theory/ordinal_notation.lean
@@ -275,7 +275,7 @@ begin
   have := mt repr_inj.1 (λ h, by injection h : oadd e n a ≠ 0),
   have L := le_of_not_lt (λ l, not_le_of_lt (h.below_of_lt l).repr_lt (le_of_dvd this d)),
   simp at d,
-  exact ⟨L, (dvd_add_iff $ dvd_mul_of_dvd _ $ power_dvd_power _ L).1 d⟩
+  exact ⟨L, (dvd_add_iff $ dvd_mul_of_dvd_left (power_dvd_power _ L) _).1 d⟩
 end
 
 theorem NF.of_dvd_omega {e n a} (h : NF (oadd e n a)) :
@@ -611,7 +611,7 @@ begin
   cases e : split' o with a n,
   rw split_eq_scale_split' e at h,
   injection h, subst o',
-  cases NF_repr_split' e, resetI, simp [dvd_mul]
+  cases NF_repr_split' e, resetI, simp
 end
 
 theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) : repr a + m < ω ^ repr e :=
@@ -728,8 +728,8 @@ begin
   ... = (ω0 ^ k * α' + R) * α' + (ω0 ^ k * α' + R) * m : _
   ... = (α' + m) ^ succ k.succ : by rw [← ordinal.mul_add, ← nat_cast_succ, power_succ, IH.2],
   congr' 1,
-  { have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd _
-      (by simpa using power_dvd_power ω (one_le_iff_ne_zero.2 e0))) d,
+  { have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd_left
+      (by simpa using power_dvd_power ω (one_le_iff_ne_zero.2 e0)) _) d,
     rw [ordinal.mul_add (ω0 ^ k), add_assoc, ← mul_assoc, ← power_succ,
         add_mul_limit _ (is_limit_iff_omega_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc,
         @mul_omega_dvd n (nat_cast_pos.2 n.pos) (nat_lt_omega _) _ αd],