chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

- `[nonzero_semiring α]` becomes `[semiring α] [nonzero α]`
- `[nonzero_comm_semiring α]` becomes `[comm_semiring α] [nonzero α]`
- `[nonzero_comm_ring α]` becomes `[comm_ring α] [nonzero α]`
- `no_zero_divisors` is now a `Prop`
- `units.ne_zero` (originally for `domain`) merges into `units.coe_ne_zero` (originally for `nonzero_comm_semiring`)

Author: kckennylau

src/algebra/associated.lean

@@ -18,7 +18,7 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
   refine ⟨⟨0, 0, _, _⟩, rfl⟩; apply subsingleton.elim
  end⟩
 
-@[simp] theorem not_is_unit_zero [nonzero_semiring α] : ¬ is_unit (0 : α) :=
+@[simp] theorem not_is_unit_zero [semiring α] [nonzero α] : ¬ is_unit (0 : α) :=
 mt is_unit_zero_iff.1 zero_ne_one
 
 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=

src/algebra/char_p.lean

@@ -258,10 +258,10 @@ calc r = 1 * r       : by rw one_mul
 
 end prio
 
-lemma false_of_nonzero_of_char_one [nonzero_comm_ring R] [char_p R 1] : false :=
+lemma false_of_nonzero_of_char_one [semiring R] [nonzero R] [char_p R 1] : false :=
 zero_ne_one $ show (0:R) = 1, from subsingleton.elim 0 1
 
-lemma ring_char_ne_one [nonzero_semiring R] : ring_char R ≠ 1 :=
+lemma ring_char_ne_one [semiring R] [nonzero R] : ring_char R ≠ 1 :=
 by { intros h, apply @zero_ne_one R, symmetry, rw [←nat.cast_one, ring_char.spec, h], }
 
 end char_one

src/algebra/classical_lie_algebras.lean

@@ -28,7 +28,7 @@ namespace lie_algebra
 open_locale matrix
 
 variables (n : Type u₁) (R : Type u₂)
-variables [fintype n] [decidable_eq n] [nonzero_comm_ring R]
+variables [fintype n] [decidable_eq n] [comm_ring R]
 
 local attribute [instance] matrix.lie_ring
 local attribute [instance] matrix.lie_algebra
@@ -77,7 +77,7 @@ def Eb (h : j ≠ i) : sl n R :=
 
 end elementary_basis
 
-lemma sl_non_abelian (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
+lemma sl_non_abelian [nonzero R] (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
 begin
   rcases fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩,
   let A := Eb R i j hij,

src/algebra/direct_limit.lean

@@ -497,15 +497,14 @@ variables [directed_system G f]
 
 namespace direct_limit
 
-instance nonzero_comm_ring : nonzero_comm_ring (ring.direct_limit G f) :=
+instance nonzero : nonzero (ring.direct_limit G f) :=
 { zero_ne_one := nonempty.elim (by apply_instance) $ assume i : ι, begin
     change (0 : ring.direct_limit G f) ≠ 1,
     rw ← ring.direct_limit.of_one,
     intros H, rcases ring.direct_limit.of.zero_exact H.symm with ⟨j, hij, hf⟩,
     rw is_ring_hom.map_one (f i j hij) at hf,
     exact one_ne_zero hf
-  end,
-  .. ring.direct_limit.comm_ring G f }
+  end }
 
 theorem exists_inv {p : ring.direct_limit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
 ring.direct_limit.induction_on p $ λ i x H,
@@ -529,7 +528,8 @@ protected noncomputable def field : field (ring.direct_limit G f) :=
 { inv := inv G f,
   mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
   inv_zero := dif_pos rfl,
-  .. direct_limit.nonzero_comm_ring G f }
+  .. ring.direct_limit.comm_ring G f,
+  .. direct_limit.nonzero G f }
 
 end
 

src/algebra/euclidean_domain.lean

@@ -12,9 +12,9 @@ universe u
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
-
+set_option old_structure_cmd true
 @[protect_proj without mul_left_not_lt r_well_founded]
-class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
+class euclidean_domain (α : Type u) extends comm_ring α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : α → α → α)
@@ -32,6 +32,7 @@ class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
   function from weak to strong. I've currently divided the lemmas into
   strong and weak depending on whether they require `val_le_mul_left` or not. -/
 (mul_left_not_lt : ∀ a {b}, b ≠ 0 → ¬r (a * b) a)
+(zero_ne_one : (0 : α) ≠ 1)
 end prio
 
 namespace euclidean_domain
@@ -40,6 +41,9 @@ variables [euclidean_domain α]
 
 local infix ` ≺ `:50 := euclidean_domain.r
 
+@[priority 70] -- see Note [lower instance priority]
+instance : nonzero α := ⟨euclidean_domain.zero_ne_one⟩
+
 @[priority 70] -- see Note [lower instance priority]
 instance : has_div α := ⟨euclidean_domain.quotient⟩
 
@@ -328,8 +332,6 @@ end lcm
 
 end euclidean_domain
 
-open euclidean_domain
-
 instance int.euclidean_domain : euclidean_domain ℤ :=
 { quotient := (/),
   quotient_zero := int.div_zero,
@@ -342,7 +344,9 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     exact int.mod_lt _ b0,
   mul_left_not_lt := λ a b b0, not_lt_of_ge $
     by rw [← mul_one a.nat_abs, int.nat_abs_mul];
-    exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _) }
+    exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _),
+  .. int.comm_ring,
+  .. int.nonzero }
 
 @[priority 100] -- see Note [lower instance priority]
 instance field.to_euclidean_domain {K : Type u} [field K] : euclidean_domain K :=
@@ -355,4 +359,5 @@ instance field.to_euclidean_domain {K : Type u} [field K] : euclidean_domain K :
   r_well_founded := well_founded.intro $ λ a, acc.intro _ $ λ b ⟨hb, hna⟩,
     acc.intro _ $ λ c ⟨hc, hnb⟩, false.elim $ hnb hb,
   remainder_lt := λ a b hnb, by simp [hnb],
-  mul_left_not_lt := λ a b hnb ⟨hab, hna⟩, or.cases_on (mul_eq_zero.1 hab) hna hnb }
+  mul_left_not_lt := λ a b hnb ⟨hab, hna⟩, or.cases_on (mul_eq_zero.1 hab) hna hnb,
+  .. ‹field K› }

src/algebra/field.lean

@@ -13,15 +13,19 @@ set_option old_structure_cmd true
 universe u
 variables {α : Type u}
 
-@[protect_proj, ancestor ring has_inv zero_ne_one_class]
-class division_ring (α : Type u) extends ring α, has_inv α, zero_ne_one_class α :=
+@[protect_proj, ancestor ring has_inv]
+class division_ring (α : Type u) extends ring α, has_inv α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
+(zero_ne_one : (0 : α) ≠ 1)
 
 section division_ring
 variables [division_ring α] {a b : α}
 
+instance division_ring.to_nonzero : nonzero α :=
+⟨division_ring.zero_ne_one⟩
+
 protected definition algebra.div (a b : α) : α :=
 a * b⁻¹
 
@@ -284,9 +288,10 @@ instance division_ring.to_domain : domain α :=
 end division_ring
 
 @[protect_proj, ancestor division_ring comm_ring]
-class field (α : Type u) extends comm_ring α, has_inv α, zero_ne_one_class α :=
+class field (α : Type u) extends comm_ring α, has_inv α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
+(zero_ne_one : (0 : α) ≠ 1)
 
 section field
 

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.ne_zero _), norm_unit_coe_units, mul_inv_eq_one]
+  assume h, by rw [norm_unit_mul h (units.coe_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,7 +79,7 @@ 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.ne_zero, norm_unit_coe_units],
+    by simpa only [normalize, mul_assoc, norm_unit_mul ha u.coe_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
@@ -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.ne_zero, or_false])
+    by simpa only [normalize_eq_zero, mul_eq_zero, units.coe_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 :=

src/algebra/group/with_one.lean

@@ -117,10 +117,8 @@ namespace with_zero
 instance [one : has_one α] : has_one (with_zero α) :=
 { ..one }
 
-instance [has_one α] : zero_ne_one_class (with_zero α) :=
-{ zero_ne_one := λ h, option.no_confusion h,
-  ..with_zero.has_zero,
-  ..with_zero.has_one }
+instance [has_one α] : nonzero (with_zero α) :=
+{ zero_ne_one := λ h, option.no_confusion h }
 
 lemma coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl
 
@@ -159,7 +157,8 @@ instance [monoid α] : monoid (with_zero α) :=
     | none   := rfl
     | some a := congr_arg some $ mul_one _
     end,
-  ..with_zero.zero_ne_one_class,
+  ..with_zero.has_one,
+  ..with_zero.nonzero,
   ..with_zero.semigroup }
 
 instance [comm_monoid α] : comm_monoid (with_zero α) :=

src/algebra/group_with_zero.lean

@@ -50,10 +50,13 @@ The type is required to come with an “inverse” function, and the inverse of
 
 Examples include division rings and the ordered monoids that are the
 target of valuations in general valuation theory.-/
-class group_with_zero (G₀ : Type*)
-  extends monoid_with_zero G₀, has_inv G₀, zero_ne_one_class G₀ :=
+class group_with_zero (G₀ : Type*) extends monoid_with_zero G₀, has_inv G₀ :=
 (inv_zero : (0 : G₀)⁻¹ = 0)
 (mul_inv_cancel : ∀ a:G₀, a ≠ 0 → a * a⁻¹ = 1)
+(zero_ne_one : (0 : G₀) ≠ 1)
+
+instance group_with_zero.to_nonzero (G₀ : Type*) [group_with_zero G₀] : nonzero G₀ :=
+⟨group_with_zero.zero_ne_one⟩
 
 /-- A type `G₀` is a commutative “group with zero”
 if it is a commutative monoid with zero element (distinct from `1`)

src/algebra/opposites.lean

@@ -109,20 +109,19 @@ instance [ring α] : ring (opposite α) :=
 instance [comm_ring α] : comm_ring (opposite α) :=
 { .. opposite.ring α, .. opposite.comm_semigroup α }
 
-instance [zero_ne_one_class α] : zero_ne_one_class (opposite α) :=
-{ zero_ne_one := λ h, zero_ne_one $ op_inj h,
-  .. opposite.has_zero α, .. opposite.has_one α }
+instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
+{ zero_ne_one := λ h : op (0 : α) = op 1, zero_ne_one (op_inj h) }
 
 instance [integral_domain α] : integral_domain (opposite α) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op (_ * _) = op (0:α)),
     or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ op_inj H)
       (λ hy, or.inr $ unop_inj $ hy) (λ hx, or.inl $ unop_inj $ hx),
-  .. opposite.comm_ring α, .. opposite.zero_ne_one_class α }
+  .. opposite.comm_ring α, .. opposite.nonzero α }
 
 instance [field α] : field (opposite α) :=
 { mul_inv_cancel := λ x hx, unop_inj $ inv_mul_cancel $ λ hx', hx $ unop_inj hx',
   inv_zero := unop_inj inv_zero,
-  .. opposite.comm_ring α, .. opposite.zero_ne_one_class α, .. opposite.has_inv α }
+  .. opposite.comm_ring α, .. opposite.nonzero α, .. opposite.has_inv α }
 
 @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl
 @[simp] lemma unop_zero [has_zero α] : unop (0 : αᵒᵖ) = 0 := rfl