chore(number_theory/*): Weaken assumptions (#13443)

Follow @alexjbest's generalization linter to weaken typeclass assumptions in number theory.

src/number_theory/arithmetic_function.lean

@@ -408,7 +408,8 @@ lemma pmul_comm [comm_monoid_with_zero R] (f g : arithmetic_function R) :
   f.pmul g = g.pmul f :=
 by { ext, simp [mul_comm] }
 
-variable [semiring R]
+section non_assoc_semiring
+variable [non_assoc_semiring R]
 
 @[simp]
 lemma pmul_zeta (f : arithmetic_function R) : f.pmul ↑ζ = f :=
@@ -426,6 +427,10 @@ begin
   simp [nat.succ_ne_zero],
 end
 
+end non_assoc_semiring
+
+variables [semiring R]
+
 /-- This is the pointwise power of `arithmetic_function`s. -/
 def ppow (f : arithmetic_function R) (k : ℕ) :
   arithmetic_function R :=
@@ -775,7 +780,7 @@ end
 
 open unique_factorization_monoid
 
-@[simp] lemma coe_moebius_mul_coe_zeta [comm_ring R] : (μ * ζ : arithmetic_function R) = 1 :=
+@[simp] lemma coe_moebius_mul_coe_zeta [ring R] : (μ * ζ : arithmetic_function R) = 1 :=
 begin
   ext x,
   cases x,
@@ -883,15 +888,14 @@ begin
     rw (if_neg (ne_of_gt (nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)))) },
 end
 
-/-- Möbius inversion for functions to a `comm_ring`. -/
-theorem sum_eq_iff_sum_mul_moebius_eq [comm_ring R] {f g : ℕ → R} :
+/-- Möbius inversion for functions to a `ring`. -/
+theorem sum_eq_iff_sum_mul_moebius_eq [ring R] {f g : ℕ → R} :
   (∀ (n : ℕ), 0 < n → ∑ i in (n.divisors), f i = g n) ↔
     ∀ (n : ℕ), 0 < n → ∑ (x : ℕ × ℕ) in n.divisors_antidiagonal, (μ x.fst : R) * g x.snd = f n :=
 begin
   rw sum_eq_iff_sum_smul_moebius_eq,
   apply forall_congr,
-  intro a,
-  apply imp_congr (iff.refl _) (eq.congr_left (sum_congr rfl (λ x hx, _))),
+  refine λ a, imp_congr_right (λ _, (sum_congr rfl $ λ x hx, _).congr_left),
   rw [zsmul_eq_mul],
 end
 

src/number_theory/class_number/admissible_card_pow_degree.lean

@@ -24,11 +24,11 @@ namespace polynomial
 open_locale polynomial
 open absolute_value real
 
-variables {Fq : Type*} [field Fq] [fintype Fq]
+variables {Fq : Type*} [fintype Fq]
 
-/-- If `A` is a family of enough low-degree polynomials over a finite field, there is a
+/-- If `A` is a family of enough low-degree polynomials over a finite semiring, there is a
 pair of equal elements in `A`. -/
-lemma exists_eq_polynomial {d : ℕ} {m : ℕ} (hm : fintype.card Fq ^ d ≤ m) (b : Fq[X])
+lemma exists_eq_polynomial [semiring Fq] {d : ℕ} {m : ℕ} (hm : fintype.card Fq ^ d ≤ m) (b : Fq[X])
   (hb : nat_degree b ≤ d) (A : fin m.succ → Fq[X]) (hA : ∀ i, degree (A i) < degree b) :
   ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀ :=
 begin
@@ -53,10 +53,10 @@ begin
   exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb
 end
 
-/-- If `A` is a family of enough low-degree polynomials over a finite field,
+/-- If `A` is a family of enough low-degree polynomials over a finite ring,
 there is a pair of elements in `A` (with different indices but not necessarily
 distinct), such that their difference has small degree. -/
-lemma exists_approx_polynomial_aux {d : ℕ} {m : ℕ} (hm : fintype.card Fq ^ d ≤ m)
+lemma exists_approx_polynomial_aux [ring Fq] {d : ℕ} {m : ℕ} (hm : fintype.card Fq ^ d ≤ m)
   (b : Fq[X]) (A : fin m.succ → Fq[X]) (hA : ∀ i, degree (A i) < degree b) :
   ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(nat_degree b - d) :=
 begin
@@ -94,6 +94,8 @@ begin
   convert congr_fun i_eq.symm ⟨nat_degree b - j.succ, hj⟩
 end
 
+variables [field Fq]
+
 /-- If `A` is a family of enough low-degree polynomials over a finite field,
 there is a pair of elements in `A` (with different indices but not necessarily
 distinct), such that the difference of their remainders is close together. -/

src/number_theory/class_number/finite.lean

@@ -90,7 +90,7 @@ end
 
 /-- If the `R`-integral element `a : S` has coordinates `< y` with respect to some basis `b`,
 its norm is strictly less than `norm_bound abv b * y ^ dim S`. -/
-lemma norm_lt {T : Type*} [linear_ordered_comm_ring T]
+lemma norm_lt {T : Type*} [linear_ordered_ring T]
   (a : S) {y : T} (hy : ∀ k, (abv (bS.repr a k) : T) < y) :
   (abv (algebra.norm R a) : T) < norm_bound abv bS * y ^ fintype.card ι :=
 begin

src/number_theory/liouville/basic.lean

@@ -87,7 +87,7 @@ It is stated in more general form than needed: in the intended application, `Z =
 root of `f`, `ε` is small, `M` is a bound on the Lipschitz constant of `f` near `α`, `n` is
 the degree of the polynomial `f`.
 -/
-lemma exists_one_le_pow_mul_dist {Z N R : Type*} [metric_space R]
+lemma exists_one_le_pow_mul_dist {Z N R : Type*} [pseudo_metric_space R]
   {d : N → ℝ} {j : Z → N → R} {f : R → R} {α : R} {ε M : ℝ}
 -- denominators are positive
   (d0 : ∀ (a : N), 1 ≤ d a)

src/number_theory/padics/ring_homs.lean

@@ -465,7 +465,7 @@ section lift
 
 open cau_seq padic_seq
 
-variables {R : Type*} [comm_ring R] (f : Π k : ℕ, R →+* zmod (p^k))
+variables {R : Type*} [non_assoc_semiring R] (f : Π k : ℕ, R →+* zmod (p^k))
   (f_compat : ∀ k1 k2 (hk : k1 ≤ k2), (zmod.cast_hom (pow_dvd_pow p hk) _).comp (f k2) = f k1)
 
 omit hp_prime
@@ -687,7 +687,7 @@ begin
   { rintro rfl _, refl }
 end
 
-lemma to_zmod_pow_eq_iff_ext {R : Type*} [comm_ring R] {g g' : R →+* ℤ_[p]} :
+lemma to_zmod_pow_eq_iff_ext {R : Type*} [non_assoc_semiring R] {g g' : R →+* ℤ_[p]} :
   (∀ n, (to_zmod_pow n).comp g = (to_zmod_pow n).comp g') ↔ g = g' :=
 begin
   split,

src/number_theory/zsqrtd/basic.lean

@@ -725,14 +725,16 @@ begin
     exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _) }
 end
 
-variables {R : Type} [comm_ring R]
+variables {R : Type}
 
-@[ext] lemma hom_ext {d : ℤ} (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) : f = g :=
+@[ext] lemma hom_ext [ring R] {d : ℤ} (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) : f = g :=
 begin
   ext ⟨x_re, x_im⟩,
   simp [decompose, h],
 end
 
+variables [comm_ring R]
+
 /-- The unique `ring_hom` from `ℤ√d` to a ring `R`, constructed by replacing `√d` with the provided
 root. Conversely, this associates to every mapping `ℤ√d →+* R` a value of `√d` in `R`. -/
 @[simps]