refactor(data/polynomial,ring_theory): use big operators for polynomi…

…als (#6616)

This untangles some more definitions on polynomials from finsupp.  This uses the same approach as in #6605.

src/data/polynomial/div.lean

@@ -16,7 +16,7 @@ We also define `root_multiplicity`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
+open_locale classical big_operators
 
 open finset
 
@@ -30,27 +30,18 @@ variables [semiring R] {p q : polynomial R}
 /-- `div_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
   It can be used in a semiring where the usual division algorithm is not possible -/
 def div_X (p : polynomial R) : polynomial R :=
-{ to_fun := λ n, p.coeff (n + 1),
-  support := ⟨(p.support.filter (> 0)).1.map (λ n, n - 1),
-    multiset.nodup_map_on begin
-        simp only [finset.mem_def.symm, finset.mem_erase, finset.mem_filter],
-        assume x hx y hy hxy,
-        rwa [← @add_right_cancel_iff _ _ 1, nat.sub_add_cancel hx.2,
-          nat.sub_add_cancel hy.2] at hxy
-      end
-      (p.support.filter (> 0)).2⟩,
-  mem_support_to_fun := λ n,
-    suffices (∃ (a : ℕ), (¬coeff p a = 0 ∧ a > 0) ∧ a - 1 = n) ↔
-      ¬coeff p (n + 1) = 0,
-    by simpa [finset.mem_def.symm],
-    ⟨λ ⟨a, ha⟩, by rw [← ha.2, nat.sub_add_cancel ha.1.2]; exact ha.1.1,
-      λ h, ⟨n + 1, ⟨h, nat.succ_pos _⟩, nat.succ_sub_one _⟩⟩ }
+∑ n in Ico 0 p.nat_degree, monomial n (p.coeff (n + 1))
+
+@[simp] lemma coeff_div_X : (div_X p).coeff n = p.coeff (n+1) :=
+begin
+  simp only [div_X, coeff_monomial, true_and, finset_sum_coeff, not_lt,
+    Ico.mem, zero_le, finset.sum_ite_eq', ite_eq_left_iff],
+  intro h,
+  rw coeff_eq_zero_of_nat_degree_lt (nat.lt_succ_of_le h)
+end
 
 lemma div_X_mul_X_add (p : polynomial R) : div_X p * X + C (p.coeff 0) = p :=
-ext $ λ n,
-  nat.cases_on n
-   (by simp)
-   (by simp [coeff_C, nat.succ_ne_zero, coeff_mul_X, div_X])
+ext $ by rintro ⟨_|_⟩; simp [coeff_C, nat.succ_ne_zero, coeff_mul_X]
 
 @[simp] lemma div_X_C (a : R) : div_X (C a) = 0 :=
 ext $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
@@ -60,7 +51,7 @@ lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
   λ h, by rw [h, div_X_C]⟩
 
 lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
-ext $ by simp [div_X]
+ext $ by simp
 
 lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
 by haveI := nontrivial.of_polynomial_ne hp0;

src/data/polynomial/integral_normalization.lean

@@ -12,9 +12,7 @@ import data.polynomial.monic
 We define `integral_normalization`, which relate arbitrary polynomials to monic ones.
 -/
 
-noncomputable theory
-
-open finsupp
+open_locale big_operators
 
 namespace polynomial
 universes u v y
@@ -31,27 +29,34 @@ a monic polynomial with root `leading_coeff f * z`.
 Moreover, `integral_normalization 0 = 0`.
 -/
 noncomputable def integral_normalization (f : polynomial R) : polynomial R :=
-on_finset f.support
-  (λ i, if f.degree = i then 1 else coeff f i * f.leading_coeff ^ (f.nat_degree - 1 - i))
-  begin
-    intros i h,
-    apply mem_support_iff.mpr,
-    split_ifs at h with hi,
-    { exact coeff_ne_zero_of_eq_degree hi },
-    { exact left_ne_zero_of_mul h },
-  end
+∑ i in f.support, monomial i (if f.degree = i then 1 else
+  coeff f i * f.leading_coeff ^ (f.nat_degree - 1 - i))
+
+@[simp] lemma integral_normalization_zero :
+  integral_normalization (0 : polynomial R) = 0 :=
+by simp [integral_normalization]
+
+lemma integral_normalization_coeff {f : polynomial R} {i : ℕ} :
+  (integral_normalization f).coeff i =
+    if f.degree = i then 1 else coeff f i * f.leading_coeff ^ (f.nat_degree - 1 - i) :=
+have f.coeff i = 0 → f.degree ≠ i, from λ hc hd, coeff_ne_zero_of_eq_degree hd hc,
+by simp [integral_normalization, coeff_monomial, this, mem_support_iff] {contextual := tt}
+
+lemma integral_normalization_support {f : polynomial R} :
+  (integral_normalization f).support ⊆ f.support :=
+by { intro, simp [integral_normalization, coeff_monomial, mem_support_iff] {contextual := tt} }
 
 lemma integral_normalization_coeff_degree {f : polynomial R} {i : ℕ} (hi : f.degree = i) :
   (integral_normalization f).coeff i = 1 :=
-if_pos hi
+by rw [integral_normalization_coeff, if_pos hi]
 
 lemma integral_normalization_coeff_nat_degree {f : polynomial R} (hf : f ≠ 0) :
   (integral_normalization f).coeff (nat_degree f) = 1 :=
 integral_normalization_coeff_degree (degree_eq_nat_degree hf)
 
 lemma integral_normalization_coeff_ne_degree {f : polynomial R} {i : ℕ} (hi : f.degree ≠ i) :
   coeff (integral_normalization f) i = coeff f i * f.leading_coeff ^ (f.nat_degree - 1 - i) :=
-if_neg hi
+by rw [integral_normalization_coeff, if_neg hi]
 
 lemma integral_normalization_coeff_ne_nat_degree
   {f : polynomial R} {i : ℕ} (hi : i ≠ nat_degree f) :
@@ -60,53 +65,42 @@ integral_normalization_coeff_ne_degree (degree_ne_of_nat_degree_ne hi.symm)
 
 lemma monic_integral_normalization {f : polynomial R} (hf : f ≠ 0) :
   monic (integral_normalization f) :=
-begin
-  apply monic_of_degree_le f.nat_degree,
-  { refine finset.sup_le (λ i h, _),
-    rw [integral_normalization, mem_support_iff, coeff, on_finset_apply] at h,
-    split_ifs at h with hi,
-    { exact le_trans (le_of_eq hi.symm) degree_le_nat_degree },
-    { erw [with_bot.some_le_some],
-      apply le_nat_degree_of_ne_zero,
-      exact left_ne_zero_of_mul h } },
-  { exact integral_normalization_coeff_nat_degree hf }
-end
+monic_of_degree_le f.nat_degree
+  (finset.sup_le $ λ i h, with_bot.coe_le_coe.2 $
+    le_nat_degree_of_mem_supp i $ integral_normalization_support h)
+  (integral_normalization_coeff_nat_degree hf)
 
 end semiring
 
 section domain
 variables [integral_domain R]
 
-@[simp] lemma support_integral_normalization {f : polynomial R} (hf : f ≠ 0) :
+@[simp] lemma support_integral_normalization {f : polynomial R} :
   (integral_normalization f).support = f.support :=
 begin
+  by_cases hf : f = 0, {simp [hf]},
   ext i,
-  simp only [integral_normalization, coeff, on_finset_apply, mem_support_iff],
-  split_ifs with hi,
-  { simp only [ne.def, not_false_iff, true_iff, one_ne_zero, hi],
-    exact coeff_ne_zero_of_eq_degree hi },
-  split,
-  { intro h,
-    exact left_ne_zero_of_mul h },
-  { intro h,
-    refine mul_ne_zero h (pow_ne_zero _ _),
-    exact λ h, hf (leading_coeff_eq_zero.mp h) }
+  refine ⟨λ h, integral_normalization_support h, _⟩,
+  simp only [integral_normalization_coeff, mem_support_iff],
+  intro hfi,
+  split_ifs with hi; simp [hfi, hi, pow_ne_zero _ (leading_coeff_ne_zero.mpr hf)]
 end
 
 variables [comm_ring S]
 
-lemma integral_normalization_eval₂_eq_zero {p : polynomial R} (hp : p ≠ 0) (f : R →+* S)
+lemma integral_normalization_eval₂_eq_zero {p : polynomial R} (f : R →+* S)
   {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) :
   eval₂ f (z * f p.leading_coeff) (integral_normalization p) = 0 :=
 calc eval₂ f (z * f p.leading_coeff) (integral_normalization p)
     = p.support.attach.sum
         (λ i, f (coeff (integral_normalization p) i.1 * p.leading_coeff ^ i.1) * z ^ i.1) :
-      by { rw [eval₂, sum_def, support_integral_normalization hp],
+      by { rw [eval₂, sum_def, support_integral_normalization],
            simp only [mul_comm z, mul_pow, mul_assoc, ring_hom.map_pow, ring_hom.map_mul],
            exact finset.sum_attach.symm }
 ... = p.support.attach.sum
         (λ i, f (coeff p i.1 * p.leading_coeff ^ (nat_degree p - 1)) * z ^ i.1) :
       begin
+        by_cases hp : p = 0, {simp [hp]},
         have one_le_deg : 1 ≤ nat_degree p :=
           nat.succ_le_of_lt (nat_degree_pos_of_eval₂_root hp f hz inj),
         congr' with i,
@@ -116,21 +110,21 @@ calc eval₂ f (z * f p.leading_coeff) (integral_normalization p)
               nat.sub_add_cancel one_le_deg],
           exact degree_eq_nat_degree hp },
         { have : i.1 ≤ p.nat_degree - 1 := nat.le_pred_of_lt (lt_of_le_of_ne
-            (le_nat_degree_of_ne_zero (finsupp.mem_support_iff.mp i.2)) hi),
+            (le_nat_degree_of_ne_zero (mem_support_iff.mp i.2)) hi),
           rw [integral_normalization_coeff_ne_nat_degree hi, mul_assoc, ←pow_add,
               nat.sub_add_cancel this] }
       end
 ... = f p.leading_coeff ^ (nat_degree p - 1) * eval₂ f z p :
-      by { simp_rw [eval₂, finsupp.sum, λ i, mul_comm (coeff p i), ring_hom.map_mul,
+      by { simp_rw [eval₂, sum_def, λ i, mul_comm (coeff p i), ring_hom.map_mul,
                     ring_hom.map_pow, mul_assoc, ←finset.mul_sum],
            congr' 1,
            exact @finset.sum_attach _ _ p.support _ (λ i, f (p.coeff i) * z ^ i) }
 ... = 0 : by rw [hz, _root_.mul_zero]
 
-lemma integral_normalization_aeval_eq_zero [algebra R S] {f : polynomial R} (hf : f ≠ 0)
+lemma integral_normalization_aeval_eq_zero [algebra R S] {f : polynomial R}
   {z : S} (hz : aeval z f = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
   aeval (z * algebra_map R S f.leading_coeff) (integral_normalization f) = 0 :=
-integral_normalization_eval₂_eq_zero hf (algebra_map R S) hz inj
+integral_normalization_eval₂_eq_zero (algebra_map R S) hz inj
 
 end domain
 

src/ring_theory/algebraic.lean

@@ -131,7 +131,7 @@ begin
   have x_integral : is_integral R (z * algebra_map R S a) :=
     ⟨ p.integral_normalization,
       monic_integral_normalization p_ne_zero,
-      integral_normalization_aeval_eq_zero p_ne_zero px inj ⟩,
+      integral_normalization_aeval_eq_zero px inj ⟩,
   refine ⟨⟨_, x_integral⟩, ⟨_, y_integral⟩, _, rfl⟩,
   exact λ h, a_ne_zero (inj _ (subtype.ext_iff_val.mp h))
 end

src/ring_theory/polynomial/rational_root.lean

@@ -102,7 +102,8 @@ begin
   apply dvd_term_of_is_root_of_dvd_terms _ (num_is_root_scale_roots_of_aeval_eq_zero f hr),
   intros j hj,
   by_cases h : j < p.nat_degree,
-  { refine dvd_mul_of_dvd_left (dvd_mul_of_dvd_right _ _) _,
+  { rw coeff_scale_roots,
+    refine dvd_mul_of_dvd_left (dvd_mul_of_dvd_right _ _) _,
     convert pow_dvd_pow _ (nat.succ_le_iff.mpr (nat.lt_sub_left_of_add_lt _)),
     { exact (pow_one _).symm },
     simpa using h },

src/ring_theory/polynomial/scale_roots.lean

@@ -20,16 +20,15 @@ variables {A K R S : Type*} [integral_domain A] [field K] [comm_ring R] [comm_ri
 variables {M : submonoid A}
 
 open finsupp polynomial
+open_locale big_operators
 
 /-- `scale_roots p s` is a polynomial with root `r * s` for each root `r` of `p`. -/
 noncomputable def scale_roots (p : polynomial R) (s : R) : polynomial R :=
-on_finset p.support
-  (λ i, coeff p i * s ^ (p.nat_degree - i))
-  (λ i h, polynomial.mem_support_iff.mpr (left_ne_zero_of_mul h))
+∑ i in p.support, monomial i (p.coeff i * s ^ (p.nat_degree - i))
 
 @[simp] lemma coeff_scale_roots (p : polynomial R) (s : R) (i : ℕ) :
   (scale_roots p s).coeff i = coeff p i * s ^ (p.nat_degree - i) :=
-rfl
+by simp [scale_roots, coeff_monomial] {contextual := tt}
 
 lemma coeff_scale_roots_nat_degree (p : polynomial R) (s : R) :
   (scale_roots p s).coeff p.nat_degree = p.leading_coeff :=
@@ -90,7 +89,7 @@ lemma scale_roots_eval₂_eq_zero {p : polynomial S} (f : S →+* R)
   eval₂ f (f s * r) (scale_roots p s) = 0 :=
 calc eval₂ f (f s * r) (scale_roots p s) =
   (scale_roots p s).support.sum (λ i, f (coeff p i * s ^ (p.nat_degree - i)) * (f s * r) ^ i) :
-  eval₂_eq_sum
+  by simp [eval₂_eq_sum, sum_def]
 ... = p.support.sum (λ i, f (coeff p i * s ^ (p.nat_degree - i)) * (f s * r) ^ i) :
   finset.sum_subset (support_scale_roots_le p s)
   (λ i hi hi', let this : coeff p i * s ^ (p.nat_degree - i) = 0 :=
@@ -103,7 +102,7 @@ calc eval₂ f (f s * r) (scale_roots p s) =
   (λ i hi, by { rw [mul_assoc, mul_left_comm, nat.sub_add_cancel],
                 exact le_nat_degree_of_ne_zero (polynomial.mem_support_iff.mp hi) })
 ... = f s ^ p.nat_degree * p.support.sum (λ (i : ℕ), (f (p.coeff i) * r ^ i)) : finset.mul_sum.symm
-... = f s ^ p.nat_degree * eval₂ f r p : by { rw [eval₂_eq_sum], refl }
+... = f s ^ p.nat_degree * eval₂ f r p : by { simp [eval₂_eq_sum, sum_def] }
 ... = 0 : by rw [hr, _root_.mul_zero]
 
 lemma scale_roots_aeval_eq_zero [algebra S R] {p : polynomial S}