feat(algebra/polynomial): big_operators lemmas for polynomials (#3378)

This starts a new folder algebra/polynomial. As we refactor data/polynomial.lean, much of that content should land in this folder. 



Co-authored-by: Aaron Anderson <awainverse@gmail.com>

Author: jalex-stark

src/algebra/polynomial/basic.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2020 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson, Jalex Stark.
+-/
+import data.polynomial
+open polynomial finset
+
+/-!
+# Polynomials
+
+Eventually, much of data/polynomial.lean should land here.
+
+## Main results
+
+We relate `eval` and the constant coefficient map to `aeval`, so we can use `alg_hom` properties.
+
+We define a `monoid_hom` of type `polynomial R →* R`,
+under the assumption that `R` is an integral domain.
+- `leading_coeff_hom`
+-/
+
+universes u w
+
+noncomputable theory
+
+variables {R : Type u} {α : Type w}
+
+namespace polynomial
+
+section comm_semiring
+variables [comm_semiring R]
+
+@[simp] lemma coe_aeval_eq_eval (r : R) :
+  (aeval R R r : polynomial R → R) = eval r := rfl
+
+lemma coeff_zero_eq_aeval_zero (p : polynomial R) : p.coeff 0 = aeval R R 0 p :=
+by { rw coeff_zero_eq_eval_zero, rw coe_aeval_eq_eval, }
+
+end comm_semiring
+
+section integral_domain
+variable [integral_domain R]
+
+/-- `polynomial.leading_coeff` bundled as a `monoid_hom` when `R` is an `integral_domain`, and thus
+  `leading_coeff` is multiplicative -/
+def leading_coeff_hom : polynomial R →* R :=
+{ to_fun := leading_coeff,
+  map_one' := by simp,
+  map_mul' := leading_coeff_mul }
+
+@[simp] lemma leading_coeff_hom_apply (p : polynomial R) :
+  leading_coeff_hom p = leading_coeff p := rfl
+
+end integral_domain
+end polynomial

src/algebra/polynomial/big_operators.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2020 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson, Jalex Stark.
+-/
+import algebra.polynomial.basic
+open polynomial finset
+
+/-!
+# Polynomials
+
+Lemmas for the interaction between polynomials and ∑ and ∏.
+
+## Main results
+
+- `nat_degree_prod_eq_of_monic` : the degree of a product of monic polynomials is the product of
+    degrees. We prove this only for [comm_semiring R],
+    but it ought to be true for [semiring R] and list.prod.
+- `nat_degree_prod_eq` : for polynomials over an integral domain,
+    the degree of the product is the sum of degrees
+- `leading_coeff_prod` : for polynomials over an integral domain,
+    the leading coefficient is the product of leading coefficients
+-/
+
+open_locale big_operators
+
+universes u w
+
+variables {R : Type u} {α : Type w}
+
+namespace polynomial
+
+variable (s : finset α)
+
+section comm_semiring
+variables [comm_semiring R] (f : α → polynomial R)
+
+lemma nat_degree_prod_le : (∏ i in s, f i).nat_degree ≤ ∑ i in s, (f i).nat_degree :=
+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,
+end
+
+/-- The leading coefficient of a product of polynomials is equal to the product of the leading coefficients, provided that this product is nonzero.
+See `leading_coeff_prod` (without the `'`) for a version for integral domains, 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 :=
+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 },
+end
+
+/-- The degree of a product of polynomials is equal to the product of the degrees, provided that the product of leading coefficients is nonzero.
+See `nat_degree_prod_eq` (without the `'`) for a version for integral domains, where this condition is automatically satisfied. -/
+lemma nat_degree_prod_eq' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
+  (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
+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_eq', rw hs,
+  apply right_ne_zero_of_mul h,
+  rwa polynomial.leading_coeff_prod', apply right_ne_zero_of_mul h,
+end
+
+lemma monic_prod_of_monic :
+  (∀ a : α, a ∈ s → monic (f a)) → monic (∏ i in s, f i) :=
+by { apply prod_induction, apply monic_mul, apply monic_one }
+
+lemma nat_degree_prod_eq_of_monic [nontrivial R] (h : ∀ i : α, i ∈ s → (f i).monic) :
+  (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
+begin
+  apply nat_degree_prod_eq',
+  suffices : ∏ (i : α) in s, (f i).leading_coeff = 1, { rw this, simp },
+  rw prod_eq_one, intros, apply h, assumption,
+end
+
+end comm_semiring
+
+section integral_domain
+variables [integral_domain R] (f : α → polynomial R)
+
+lemma nat_degree_prod_eq (h : ∀ i ∈ s, f i ≠ 0) :
+  (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
+begin
+  apply nat_degree_prod_eq', rw prod_ne_zero_iff,
+  intros x hx, simp [h x hx],
+end
+
+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 }
+
+end integral_domain
+end polynomial