chore(field_theory/finite/polynomial): tidy + remove nolints (#13645)

Some of these definitions only make full sense over a field (for example the indicator function can be nonsensical in non-field rings) but there's also no reason not to define them more generally. This removes all `nolint`s related to this file, and all of the generalisation linter suggestions too.

src/field_theory/finite/polynomial.lean

@@ -27,8 +27,7 @@ section frobenius
 
 variables {p : ℕ} [fact p.prime]
 
-lemma frobenius_zmod (f : mv_polynomial σ (zmod p)) :
-  frobenius _ p f = expand p f :=
+lemma frobenius_zmod (f : mv_polynomial σ (zmod p)) : frobenius _ p f = expand p f :=
 begin
   apply induction_on f,
   { intro a, rw [expand_C, frobenius_def, ← C_pow, zmod.pow_card], },
@@ -37,8 +36,7 @@ begin
     intros _ _ hf, rw [hf, frobenius_def], },
 end
 
-lemma expand_zmod (f : mv_polynomial σ (zmod p)) :
-  expand p f = f ^ p :=
+lemma expand_zmod (f : mv_polynomial σ (zmod p)) : expand p f = f ^ p :=
 (frobenius_zmod _).symm
 
 end frobenius
@@ -52,33 +50,26 @@ open_locale big_operators classical
 open set linear_map submodule
 
 variables {K : Type*} {σ : Type*}
-variables [field K] [fintype K] [fintype σ]
 
-def indicator (a : σ → K) : mv_polynomial σ K :=
-∏ n, (1 - (X n - C (a n))^(fintype.card K - 1))
+section indicator
+
+variables [fintype K] [fintype σ]
+
+/-- Over a field, this is the indicator function as an `mv_polynomial`. -/
+def indicator [comm_ring K] (a : σ → K) : mv_polynomial σ K :=
+∏ n, (1 - (X n - C (a n)) ^ (fintype.card K - 1))
+
+section comm_ring
+
+variables [comm_ring K]
 
 lemma eval_indicator_apply_eq_one (a : σ → K) :
   eval a (indicator a) = 1 :=
-have 0 < fintype.card K - 1,
-begin
-  rw [← fintype.card_units, fintype.card_pos_iff],
-  exact ⟨1⟩
-end,
-by { simp only [indicator, (eval a).map_prod, ring_hom.map_sub,
-    (eval a).map_one, (eval a).map_pow, eval_X, eval_C,
-    sub_self, zero_pow this, sub_zero, finset.prod_const_one] }
-
-lemma eval_indicator_apply_eq_zero (a b : σ → K) (h : a ≠ b) :
-  eval a (indicator b) = 0 :=
-have ∃i, a i ≠ b i, by rwa [(≠), function.funext_iff, not_forall] at h,
 begin
-  rcases this with ⟨i, hi⟩,
-  simp only [indicator, (eval a).map_prod, ring_hom.map_sub,
-    (eval a).map_one, (eval a).map_pow, eval_X, eval_C,
-    sub_self, finset.prod_eq_zero_iff],
-  refine ⟨i, finset.mem_univ _, _⟩,
-  rw [finite_field.pow_card_sub_one_eq_one, sub_self],
-  rwa [(≠), sub_eq_zero],
+  nontriviality,
+  have : 0 < fintype.card K - 1 := tsub_pos_of_lt fintype.one_lt_card,
+  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C,
+             sub_self, zero_pow this, sub_zero, finset.prod_const_one]
 end
 
 lemma degrees_indicator (c : σ → K) :
@@ -109,16 +100,34 @@ begin
   { rw [multiset.count_singleton_self, mul_one] }
 end
 
+end comm_ring
+
+variables [field K]
+
+lemma eval_indicator_apply_eq_zero (a b : σ → K) (h : a ≠ b) :
+  eval a (indicator b) = 0 :=
+begin
+  obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [(≠), function.funext_iff, not_forall] at h,
+  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C,
+             sub_self, finset.prod_eq_zero_iff],
+  refine ⟨i, finset.mem_univ _, _⟩,
+  rw [finite_field.pow_card_sub_one_eq_one, sub_self],
+  rwa [(≠), sub_eq_zero],
+end
+
+end indicator
+
 section
 variables (K σ)
-def evalₗ : mv_polynomial σ K →ₗ[K] (σ → K) → K :=
+
+/-- `mv_polynomial.eval` as a `K`-linear map. -/
+@[simps] def evalₗ [comm_semiring K] : mv_polynomial σ K →ₗ[K] (σ → K) → K :=
 { to_fun := λ p e, eval e p,
   map_add' := λ p q, by { ext x, rw ring_hom.map_add, refl, },
   map_smul' := λ a p, by { ext e, rw [smul_eq_C_mul, ring_hom.map_mul, eval_C], refl } }
 end
 
-lemma evalₗ_apply (p : mv_polynomial σ K) (e : σ → K) : evalₗ K σ p e = eval e p :=
-rfl
+variables [field K] [fintype K] [fintype σ]
 
 lemma map_restrict_dom_evalₗ : (restrict_degree σ K (fintype.card K - 1)).map (evalₗ K σ) = ⊤ :=
 begin
@@ -130,12 +139,12 @@ begin
       pi.smul_apply, linear_map.map_smul],
     simp only [evalₗ_apply],
     transitivity,
-    refine finset.sum_eq_single n _ _,
-    { assume b _ h,
-      rw [eval_indicator_apply_eq_zero _ _ h.symm, smul_zero] },
-    { assume h, exact (h $ finset.mem_univ n).elim },
+    refine finset.sum_eq_single n (λ b _ h, _) _,
+    { rw [eval_indicator_apply_eq_zero _ _ h.symm, smul_zero] },
+    { exact λ h, (h $ finset.mem_univ n).elim },
     { rw [eval_indicator_apply_eq_one, smul_eq_mul, mul_one] } }
 end
+
 end mv_polynomial
 
 namespace mv_polynomial
@@ -144,16 +153,30 @@ open_locale classical cardinal
 open linear_map submodule
 
 universe u
-variables (σ : Type u) (K : Type u) [fintype σ] [field K] [fintype K]
+variables (σ : Type u) (K : Type u) [fintype K]
 
+/-- The submodule of multivariate polynomials whose degree of each variable is strictly less
+than the cardinality of K. -/
 @[derive [add_comm_group, module K, inhabited]]
-def R : Type u := restrict_degree σ K (fintype.card K - 1)
+def R [comm_ring K] : Type u := restrict_degree σ K (fintype.card K - 1)
+
+/-- Evaluation in the `mv_polynomial.R` subtype. -/
+def evalᵢ [comm_ring K] : R σ K →ₗ[K] (σ → K) → K :=
+((evalₗ K σ).comp (restrict_degree σ K (fintype.card K - 1)).subtype)
+
+section comm_ring
+
+variables [comm_ring K]
 
 noncomputable instance decidable_restrict_degree (m : ℕ) :
   decidable_pred (∈ {n : σ →₀ ℕ | ∀i, n i ≤ m }) :=
 by simp only [set.mem_set_of_eq]; apply_instance
 
-lemma dim_R : module.rank K (R σ K) = fintype.card (σ → K) :=
+end comm_ring
+
+variables [field K]
+
+lemma dim_R [fintype σ] : module.rank K (R σ K) = fintype.card (σ → K) :=
 calc module.rank K (R σ K) =
   module.rank K (↥{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} →₀ K) :
     linear_equiv.dim_eq
@@ -174,37 +197,30 @@ calc module.rank K (R σ K) =
     (equiv.arrow_congr (equiv.refl σ) (fintype.equiv_fin K).symm).cardinal_eq
   ... = fintype.card (σ → K) : cardinal.mk_fintype _
 
-instance : finite_dimensional K (R σ K) :=
+instance [fintype σ] : finite_dimensional K (R σ K) :=
 is_noetherian.iff_fg.1 $ is_noetherian.iff_dim_lt_omega.mpr
   (by simpa only [dim_R] using cardinal.nat_lt_omega (fintype.card (σ → K)))
 
-lemma finrank_R : finite_dimensional.finrank K (R σ K) = fintype.card (σ → K) :=
+lemma finrank_R [fintype σ] : finite_dimensional.finrank K (R σ K) = fintype.card (σ → K) :=
 finite_dimensional.finrank_eq_of_dim_eq (dim_R σ K)
 
-def evalᵢ : R σ K →ₗ[K] (σ → K) → K :=
-((evalₗ K σ).comp (restrict_degree σ K (fintype.card K - 1)).subtype)
-
-lemma range_evalᵢ : (evalᵢ σ K).range = ⊤ :=
+lemma range_evalᵢ [fintype σ] : (evalᵢ σ K).range = ⊤ :=
 begin
   rw [evalᵢ, linear_map.range_comp, range_subtype],
   exact map_restrict_dom_evalₗ
 end
 
-lemma ker_evalₗ : (evalᵢ σ K).ker = ⊥ :=
+lemma ker_evalₗ [fintype σ] : (evalᵢ σ K).ker = ⊥ :=
 begin
   refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank _).mpr (range_evalᵢ _ _),
   rw [finite_dimensional.finrank_fintype_fun_eq_card, finrank_R]
 end
 
-lemma eq_zero_of_eval_eq_zero (p : mv_polynomial σ K)
+lemma eq_zero_of_eval_eq_zero  [fintype σ] (p : mv_polynomial σ K)
   (h : ∀v:σ → K, eval v p = 0) (hp : p ∈ restrict_degree σ K (fintype.card K - 1)) :
   p = 0 :=
 let p' : R σ K := ⟨p, hp⟩ in
-have p' ∈ (evalᵢ σ K).ker := by { rw [mem_ker], ext v, exact h v },
-show p'.1 = (0 : R σ K).1,
-begin
-  rw [ker_evalₗ, mem_bot] at this,
-  rw [this]
-end
+have p' ∈ (evalᵢ σ K).ker := funext h,
+show p'.1 = (0 : R σ K).1, from congr_arg _ $ by rwa [ker_evalₗ, mem_bot] at this
 
 end mv_polynomial