feat(algebra/polynomial): generalize to multiset products (#7399)

This PR generalizes the results in `algebra.polynomial.big_operators` to sums and products of multisets.

The new multiset results are stated for `multiset.prod t`, not `(multiset.map t f).prod`. To get the latter, you can simply rewrite with `multiset.map_map`.

src/algebra/polynomial/big_operators.lean

@@ -25,6 +25,7 @@ Recall that `∑` and `∏` are notation for `finset.sum` and `finset.prod` resp
 -/
 
 open finset
+open multiset
 
 open_locale big_operators
 
@@ -34,18 +35,39 @@ variables {R : Type u} {ι : Type w}
 
 namespace polynomial
 
-variable (s : finset ι)
+variables (s : finset ι)
 
 section comm_semiring
-variables [comm_semiring R] (f : ι → polynomial R)
+variables [comm_semiring R] (f : ι → polynomial R) (t : multiset (polynomial R))
+
+lemma nat_degree_multiset_prod_le :
+  t.prod.nat_degree ≤ (t.map (λ f, nat_degree f)).sum :=
+begin
+  refine multiset.induction_on t _ (λ a t ih, _), { simp },
+  rw [prod_cons, map_cons, sum_cons],
+  transitivity a.nat_degree + t.prod.nat_degree,
+  { apply polynomial.nat_degree_mul_le },
+  { exact add_le_add (le_refl _) ih }
+end
 
 lemma nat_degree_prod_le : (∏ i in s, f i).nat_degree ≤ ∑ i in s, (f i).nat_degree :=
+by simpa using nat_degree_multiset_prod_le (s.1.map f)
+
+/--
+The leading coefficient of a product of polynomials is equal to
+the product of the leading coefficients, provided that this product is nonzero.
+
+See `polynomial.leading_coeff_multiset_prod` (without the `'`) for a version for integral domains,
+where this condition is automatically satisfied.
+-/
+lemma leading_coeff_multiset_prod' (h : (t.map (λ f, leading_coeff f)).prod ≠ 0) :
+  t.prod.leading_coeff = (t.map (λ f, leading_coeff f)).prod :=
 begin
-  classical,
-  induction s using finset.induction with a s ha hs, { simp },
-  rw [prod_insert ha, sum_insert ha],
-  transitivity (f a).nat_degree + (∏ x in s, f x).nat_degree,
-  apply polynomial.nat_degree_mul_le, linarith,
+  revert h,
+  refine multiset.induction_on t _ (λ a t ih ht, _), { simp },
+  rw [map_cons, prod_cons] at ht,
+  simp only [map_cons, prod_cons],
+  rw polynomial.leading_coeff_mul'; { rwa ih, apply right_ne_zero_of_mul ht }
 end
 
 /--
@@ -57,11 +79,24 @@ where this condition is automatically satisfied.
 -/
 lemma leading_coeff_prod' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
   (∏ i in s, f i).leading_coeff = ∏ i in s, (f i).leading_coeff :=
+by simpa using leading_coeff_multiset_prod' (s.1.map f) (by simpa using h)
+
+/--
+The degree of a product of polynomials is equal to
+the sum of the degrees, provided that the product of leading coefficients is nonzero.
+
+See `polynomial.nat_degree_multiset_prod` (without the `'`) for a version for integral domains,
+where this condition is automatically satisfied.
+-/
+lemma nat_degree_multiset_prod' (h : (t.map (λ f, leading_coeff f)).prod ≠ 0) :
+  t.prod.nat_degree = (t.map (λ f, nat_degree f)).sum :=
 begin
-  classical,
-  revert h, induction s using finset.induction with a s ha hs, { simp },
-  repeat { rw prod_insert ha },
-  intro h, rw polynomial.leading_coeff_mul'; { rwa hs, apply right_ne_zero_of_mul h },
+  revert h,
+  refine multiset.induction_on t _ (λ a t ih ht, _), { simp },
+  rw [map_cons, prod_cons] at ht ⊢,
+  rw [sum_cons, polynomial.nat_degree_mul', ih],
+  { apply right_ne_zero_of_mul ht },
+  { rwa polynomial.leading_coeff_multiset_prod', apply right_ne_zero_of_mul ht },
 end
 
 /--
@@ -73,31 +108,35 @@ where this condition is automatically satisfied.
 -/
 lemma nat_degree_prod' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
   (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
+by simpa using nat_degree_multiset_prod' (s.1.map f) (by simpa using h)
+
+lemma nat_degree_multiset_prod_of_monic [nontrivial R] (h : ∀ f ∈ t, monic f) :
+  t.prod.nat_degree = (t.map (λ f, nat_degree f)).sum :=
 begin
-  classical,
-  revert h, induction s using finset.induction with a s ha hs, { simp },
-  rw [prod_insert ha, prod_insert ha, sum_insert ha],
-  intro h, rw polynomial.nat_degree_mul', rw hs,
-  apply right_ne_zero_of_mul h,
-  rwa polynomial.leading_coeff_prod', apply right_ne_zero_of_mul h,
+  apply nat_degree_multiset_prod',
+  suffices : (t.map (λ f, leading_coeff f)).prod = 1, { rw this, simp },
+  convert prod_repeat (1 : R) t.card,
+  { simp only [eq_repeat, multiset.card_map, eq_self_iff_true, true_and],
+    rintros i hi,
+    obtain ⟨i, hi, rfl⟩ := multiset.mem_map.mp hi,
+    apply h, assumption },
+  { simp }
 end
 
 lemma nat_degree_prod_of_monic [nontrivial R] (h : ∀ i ∈ s, (f i).monic) :
   (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
+by simpa using nat_degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)
+
+lemma coeff_zero_multiset_prod :
+  t.prod.coeff 0 = (t.map (λ f, coeff f 0)).prod :=
 begin
-  apply nat_degree_prod',
-  suffices : ∏ i in s, (f i).leading_coeff = 1, { rw this, simp },
-  rw prod_eq_one, intros, apply h, assumption,
+  refine multiset.induction_on t _ (λ a t ht, _), { simp },
+  rw [prod_cons, map_cons, prod_cons, polynomial.mul_coeff_zero, ht]
 end
 
 lemma coeff_zero_prod :
   (∏ i in s, f i).coeff 0 = ∏ i in s, (f i).coeff 0 :=
-begin
-  classical,
-  induction s using finset.induction with a s ha hs,
-  { simp only [coeff_one_zero, prod_empty] },
-  { simp only [ha, hs, mul_coeff_zero, not_false_iff, prod_insert] }
-end
+by simpa using coeff_zero_multiset_prod (s.1.map f)
 
 end comm_semiring
 
@@ -107,27 +146,41 @@ variables [comm_ring R]
 open monic
 -- Eventually this can be generalized with Vieta's formulas
 -- plus the connection between roots and factorization.
+lemma multiset_prod_X_sub_C_next_coeff [nontrivial R] (t : multiset R) :
+  next_coeff (t.map (λ x, X - C x)).prod = -t.sum :=
+begin
+  rw next_coeff_multiset_prod,
+  { simp only [next_coeff_X_sub_C],
+    refine t.sum_hom ⟨has_neg.neg, _, _⟩; simp [add_comm] },
+  { intros, apply monic_X_sub_C }
+end
+
 lemma prod_X_sub_C_next_coeff [nontrivial R] {s : finset ι} (f : ι → R) :
   next_coeff ∏ i in s, (X - C (f i)) = -∑ i in s, f i :=
-by { rw next_coeff_prod; { simp [monic_X_sub_C] } }
+by simpa using multiset_prod_X_sub_C_next_coeff (s.1.map f)
 
-lemma prod_X_sub_C_coeff_card_pred [nontrivial R] (s : finset ι) (f : ι → R) (hs : 0 < s.card) :
-  (∏ i in s, (X - C (f i))).coeff (s.card - 1) = - ∑ i in s, f i :=
+lemma multiset_prod_X_sub_C_coeff_card_pred [nontrivial R] (t : multiset R) (ht : 0 < t.card) :
+  (t.map (λ x, (X - C x))).prod.coeff (t.card - 1) = -t.sum :=
 begin
-  convert prod_X_sub_C_next_coeff (by assumption),
+  convert multiset_prod_X_sub_C_next_coeff (by assumption),
   rw next_coeff, split_ifs,
-  { rw nat_degree_prod_of_monic at h,
-    swap, { intros, apply monic_X_sub_C },
-    rw sum_eq_zero_iff at h,
-    simp_rw nat_degree_X_sub_C at h, contrapose! h, norm_num,
-    exact multiset.card_pos_iff_exists_mem.mp hs },
-  congr, rw nat_degree_prod_of_monic; { simp [nat_degree_X_sub_C, monic_X_sub_C] },
+  { rw nat_degree_multiset_prod_of_monic at h; simp only [multiset.mem_map] at *,
+    swap, { rintros _ ⟨_, _, rfl⟩, apply monic_X_sub_C },
+    simp_rw [multiset.sum_eq_zero_iff, multiset.mem_map] at h,
+    contrapose! h,
+    obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht,
+    exact ⟨_, ⟨_, ⟨x, hx, rfl⟩, nat_degree_X_sub_C _⟩, one_ne_zero⟩ },
+  congr, rw nat_degree_multiset_prod_of_monic; { simp [nat_degree_X_sub_C, monic_X_sub_C] },
 end
 
+lemma prod_X_sub_C_coeff_card_pred [nontrivial R] (s : finset ι) (f : ι → R) (hs : 0 < s.card) :
+  (∏ i in s, (X - C (f i))).coeff (s.card - 1) = - ∑ i in s, f i :=
+by simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)
+
 end comm_ring
 
 section no_zero_divisors
-variables [comm_ring R] [no_zero_divisors R] (f : ι → polynomial R)
+variables [comm_ring R] [no_zero_divisors R] (f : ι → polynomial R) (t : multiset (polynomial R))
 
 /--
 The degree of a product of polynomials is equal to
@@ -148,28 +201,41 @@ lemma nat_degree_multiset_prod [nontrivial R] (s : multiset (polynomial R))
   (h : (0 : polynomial R) ∉ s) :
   nat_degree s.prod = (s.map nat_degree).sum :=
 begin
-  revert h,
-  refine s.induction_on _ _,
-  { simp },
-  intros p s ih h,
-  rw [multiset.mem_cons, not_or_distrib] at h,
-  have hprod : s.prod ≠ 0 := multiset.prod_ne_zero h.2,
-  rw [multiset.prod_cons, nat_degree_mul (ne.symm h.1) hprod, ih h.2,
-    multiset.map_cons, multiset.sum_cons]
+  rw nat_degree_multiset_prod',
+  simp_rw [ne.def, multiset.prod_eq_zero_iff, multiset.mem_map, leading_coeff_eq_zero],
+  rintro ⟨_, h, rfl⟩,
+  contradiction
 end
 
 /--
 The degree of a product of polynomials is equal to
 the sum of the degrees, where the degree of the zero polynomial is ⊥.
 -/
-lemma degree_prod [nontrivial R] : (∏ i in s, f i).degree = ∑ i in s, (f i).degree :=
+lemma degree_multiset_prod [nontrivial R] :
+  t.prod.degree = (t.map (λ f, degree f)).sum :=
 begin
-  classical,
-  induction s using finset.induction with a s ha hs,
-  { simp },
-  { rw [prod_insert ha, sum_insert ha, degree_mul, hs] },
+  refine multiset.induction_on t _ (λ a t ht, _), { simp },
+  { rw [prod_cons, degree_mul, ht, map_cons, sum_cons] }
 end
 
+/--
+The degree of a product of polynomials is equal to
+the sum of the degrees, where the degree of the zero polynomial is ⊥.
+-/
+lemma degree_prod [nontrivial R] : (∏ i in s, f i).degree = ∑ i in s, (f i).degree :=
+by simpa using degree_multiset_prod (s.1.map f)
+
+/--
+The leading coefficient of a product of polynomials is equal to
+the product of the leading coefficients.
+
+See `polynomial.leading_coeff_multiset_prod'` (with a `'`) for a version for commutative semirings,
+where additionally, the product of the leading coefficients must be nonzero.
+-/
+lemma leading_coeff_multiset_prod :
+  t.prod.leading_coeff = (t.map (λ f, leading_coeff f)).prod :=
+by { rw [← leading_coeff_hom_apply, monoid_hom.map_multiset_prod], refl }
+
 /--
 The leading coefficient of a product of polynomials is equal to
 the product of the leading coefficients.
@@ -179,7 +245,7 @@ where additionally, the product of the leading coefficients must be nonzero.
 -/
 lemma leading_coeff_prod :
   (∏ i in s, f i).leading_coeff = ∏ i in s, (f i).leading_coeff :=
-by { rw ← leading_coeff_hom_apply, apply monoid_hom.map_prod }
+by simpa using leading_coeff_multiset_prod (s.1.map f)
 
 end no_zero_divisors
 end polynomial

src/data/polynomial/monic.lean

@@ -137,9 +137,22 @@ end semiring
 section comm_semiring
 variables [comm_semiring R] {p : polynomial R}
 
+lemma monic_multiset_prod_of_monic (t : multiset ι) (f : ι → polynomial R)
+  (ht : ∀ i ∈ t, monic (f i)) :
+  monic (t.map f).prod :=
+begin
+  revert ht,
+  refine t.induction_on _ _, { simp },
+  intros a t ih ht,
+  rw [multiset.map_cons, multiset.prod_cons],
+  exact monic_mul
+    (ht _ (multiset.mem_cons_self _ _))
+    (ih (λ _ hi, ht _ (multiset.mem_cons_of_mem hi)))
+end
+
 lemma monic_prod_of_monic (s : finset ι) (f : ι → polynomial R) (hs : ∀ i ∈ s, monic (f i)) :
-monic (∏ i in s, f i) :=
-prod_induction _ _ (@monic_mul _ _) monic_one hs
+  monic (∏ i in s, f i) :=
+monic_multiset_prod_of_monic s.1 f hs
 
 lemma is_unit_C {x : R} : is_unit (C x) ↔ is_unit x :=
 begin
@@ -172,20 +185,25 @@ have degree p ≤ 0,
 by rw [eq_C_of_degree_le_zero this, ← nat_degree_eq_zero_iff_degree_le_zero.2 this,
     ← leading_coeff, hm.leading_coeff, C_1]
 
-lemma monic.next_coeff_prod (s : finset ι) (f : ι → polynomial R) (h : ∀ i ∈ s, monic (f i)) :
-next_coeff (∏ i in s, f i) = ∑ i in s, next_coeff (f i) :=
+lemma monic.next_coeff_multiset_prod (t : multiset ι) (f : ι → polynomial R)
+  (h : ∀ i ∈ t, monic (f i)) :
+  next_coeff (t.map f).prod = (t.map (λ i, next_coeff (f i))).sum :=
 begin
-  classical,
-  revert h, apply finset.induction_on s,
-  { simp only [finset.not_mem_empty, forall_prop_of_true, forall_prop_of_false, finset.sum_empty,
-  finset.prod_empty, not_false_iff, forall_true_iff],
-  rw ← C_1, rw next_coeff_C_eq_zero },
-  { intros a s ha hs H,
-    rw [finset.prod_insert ha, finset.sum_insert ha, monic.next_coeff_mul, hs],
-    exacts [λ i hi, H i (mem_insert_of_mem hi), H a (mem_insert_self _ _),
-      monic_prod_of_monic _ _ (λ b bs, H _ (finset.mem_insert_of_mem bs))] }
+  revert h,
+  refine multiset.induction_on t _ (λ a t ih ht, _),
+  { simp only [multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, multiset.map_zero,
+               multiset.prod_zero, multiset.sum_zero, not_false_iff, forall_true_iff],
+    rw ← C_1, rw next_coeff_C_eq_zero },
+  { rw [multiset.map_cons, multiset.prod_cons, multiset.map_cons, multiset.sum_cons,
+        monic.next_coeff_mul, ih],
+    exacts [λ i hi, ht i (multiset.mem_cons_of_mem hi), ht a (multiset.mem_cons_self _ _),
+            monic_multiset_prod_of_monic _ _ (λ b bs, ht _ (multiset.mem_cons_of_mem bs))] }
 end
 
+lemma monic.next_coeff_prod (s : finset ι) (f : ι → polynomial R) (h : ∀ i ∈ s, monic (f i)) :
+  next_coeff (∏ i in s, f i) = ∑ i in s, next_coeff (f i) :=
+monic.next_coeff_multiset_prod s.1 f h
+
 end comm_semiring
 
 section ring