refactor(*): replace nonzero with nontrivial (#3296)

Introduce a typeclass `nontrivial` saying that a type has at least two distinct elements, and use it instead of the predicate `nonzero` requiring that `0` is different from `1`. These two predicates are equivalent in monoids with zero, which cover essentially all relevant ring-like situations, but `nontrivial` applies also to say that a vector space is nontrivial, for instance.

Along the way, fix some quirks in the alebraic hierarchy (replacing fields `zero_ne_one` in many structures with extending `nontrivial`, for instance). Also, `quadratic_reciprocity` was timing out. I guess it was just below the threshold before the refactoring, and some of the changes related to typeclass inference made it just above after the change. So, I squeeze_simped it, going from 47s to 1.7s on my computer.

Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nonsingleton/near/202865366

src/algebra/associated.lean

@@ -223,7 +223,7 @@ iff.intro
   (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, (one_mul _).symm⟩)
   (assume ⟨c, h⟩, associated.symm ⟨c, by simp [h]⟩)
 
-theorem associated_zero_iff_eq_zero [comm_semiring α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
+theorem associated_zero_iff_eq_zero [monoid_with_zero α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
 iff.intro
   (assume h, let ⟨u, h⟩ := h.symm in by simpa using h.symm)
   (assume h, h ▸ associated.refl a)
@@ -457,17 +457,30 @@ end comm_monoid
 instance [has_zero α] [monoid α] : has_zero (associates α) := ⟨⟦ 0 ⟧⟩
 instance [has_zero α] [monoid α] : has_top (associates α) := ⟨0⟩
 
-section comm_semiring
-variables [comm_semiring α]
+section comm_monoid_with_zero
+
+variables [comm_monoid_with_zero α]
 
 @[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⟩
 
-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] } }
+instance : comm_monoid_with_zero (associates α) :=
+{ 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] },
+  .. associates.comm_monoid, .. associates.has_zero }
+
+instance [nontrivial α] : nontrivial (associates α) :=
+⟨⟨0, 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⟩⟩
+
+end comm_monoid_with_zero
+
+section comm_semiring
+
+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,
@@ -547,12 +560,6 @@ instance : order_top (associates α) :=
   le_top := assume a, ⟨0, mul_zero a⟩,
   .. associates.partial_order }
 
-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 ⟩
-
 instance : no_zero_divisors (associates α) :=
 ⟨λ x y,
   (quotient.induction_on₂ x y $ assume a b h,
@@ -562,7 +569,7 @@ instance : no_zero_divisors (associates α) :=
 
 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) $
+multiset.induction_on s (by simp) $
   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 :=

src/algebra/category/CommRing/basic.lean

@@ -49,7 +49,10 @@ instance : category SemiRing := infer_instance -- short-circuit type class infer
 instance : concrete_category SemiRing := infer_instance -- short-circuit type class inference
 
 instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
-bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
+bundled_hom.mk_has_forget₂
+  (λ R hR, @monoid_with_zero.to_monoid R (@semiring.to_monoid_with_zero R hR))
+  (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
+
 instance has_forget_to_AddCommMon : has_forget₂ SemiRing AddCommMon :=
 -- can't use bundled_hom.mk_has_forget₂, since AddCommMon is an induced category
 { forget₂ :=

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 [semiring R] [nonzero R] [char_p R 1] : false :=
+lemma false_of_nonzero_of_char_one [semiring R] [nontrivial R] [char_p R 1] : false :=
 zero_ne_one $ show (0:R) = 1, from subsingleton.elim 0 1
 
-lemma ring_char_ne_one [semiring R] [nonzero R] : ring_char R ≠ 1 :=
+lemma ring_char_ne_one [semiring R] [nontrivial 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

@@ -77,9 +77,9 @@ def Eb (h : j ≠ i) : sl n R :=
 
 end elementary_basis
 
-lemma sl_non_abelian [nonzero R] (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
+lemma sl_non_abelian [nontrivial 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⟩,
+  rcases fintype.exists_pair_of_one_lt_card h with ⟨j, i, hij⟩,
   let A := Eb R i j hij,
   let B := Eb R j i hij.symm,
   intros c,

src/algebra/direct_limit.lean

@@ -497,14 +497,14 @@ variables [directed_system G f]
 
 namespace direct_limit
 
-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 }
+instance nontrivial : nontrivial (ring.direct_limit G f) :=
+⟨⟨0, 1, 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 ⟩⟩
 
 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 +529,7 @@ protected noncomputable def field : field (ring.direct_limit G f) :=
   mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
   inv_zero := dif_pos rfl,
   .. ring.direct_limit.comm_ring G f,
-  .. direct_limit.nonzero G f }
+  .. direct_limit.nontrivial G f }
 
 end
 

src/algebra/euclidean_domain.lean

@@ -14,7 +14,7 @@ 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 comm_ring α :=
+class euclidean_domain (α : Type u) extends comm_ring α, nontrivial α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : α → α → α)
@@ -32,7 +32,6 @@ class euclidean_domain (α : Type u) extends 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
@@ -41,9 +40,6 @@ 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⟩
 
@@ -351,7 +347,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     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 _),
   .. int.comm_ring,
-  .. int.nonzero }
+  .. int.nontrivial }
 
 @[priority 100] -- see Note [lower instance priority]
 instance field.to_euclidean_domain {K : Type u} [field K] : euclidean_domain K :=

src/algebra/field.lean

@@ -14,18 +14,14 @@ universe u
 variables {α : Type u}
 
 @[protect_proj, ancestor ring has_inv]
-class division_ring (α : Type u) extends ring α, has_inv α :=
+class division_ring (α : Type u) extends ring α, has_inv α, nontrivial α :=
 (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⟩
-
 instance division_ring_has_div : has_div α :=
 ⟨λ a b, a * b⁻¹⟩
 
@@ -115,10 +111,9 @@ 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 α :=
+class field (α : Type u) extends comm_ring α, has_inv α, nontrivial α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
-(zero_ne_one : (0 : α) ≠ 1)
 
 section field
 

src/algebra/group/prod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
 import algebra.group.hom
+import algebra.group_with_zero
 import data.prod
 
 /-!

src/algebra/group/with_one.lean

@@ -23,6 +23,9 @@ instance : has_one (with_one α) := ⟨none⟩
 @[to_additive]
 instance : inhabited (with_one α) := ⟨1⟩
 
+@[to_additive]
+instance [nonempty α] : nontrivial (with_one α) := option.nontrivial
+
 @[to_additive]
 instance : has_coe_t α (with_one α) := ⟨some⟩
 
@@ -117,9 +120,6 @@ namespace with_zero
 instance [one : has_one α] : has_one (with_zero α) :=
 { ..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
 
 instance [has_mul α] : mul_zero_class (with_zero α) :=
@@ -148,7 +148,7 @@ instance [comm_semigroup α] : comm_semigroup (with_zero α) :=
     end,
   ..with_zero.semigroup }
 
-instance [monoid α] : monoid (with_zero α) :=
+instance [monoid α] : monoid_with_zero (with_zero α) :=
 { one_mul := λ a, match a with
     | none   := rfl
     | some a := congr_arg some $ one_mul _
@@ -157,12 +157,12 @@ instance [monoid α] : monoid (with_zero α) :=
     | none   := rfl
     | some a := congr_arg some $ mul_one _
     end,
+  ..with_zero.mul_zero_class,
   ..with_zero.has_one,
-  ..with_zero.nonzero,
   ..with_zero.semigroup }
 
-instance [comm_monoid α] : comm_monoid (with_zero α) :=
-{ ..with_zero.monoid, ..with_zero.comm_semigroup }
+instance [comm_monoid α] : comm_monoid_with_zero (with_zero α) :=
+{ ..with_zero.monoid_with_zero, ..with_zero.comm_semigroup }
 
 definition inv [has_inv α] (x : with_zero α) : with_zero α :=
 do a ← x, return a⁻¹
@@ -260,7 +260,7 @@ instance [semiring α] : semiring (with_zero α) :=
   end,
   ..with_zero.add_comm_monoid,
   ..with_zero.mul_zero_class,
-  ..with_zero.monoid }
+  ..with_zero.monoid_with_zero }
 
 end semiring