# mathlibdocumentation

algebra.polynomial.big_operators

# Lemmas for the interaction between polynomials and ∑ and ∏. #

Recall that ∑ and ∏ are notation for finset.sum and finset.prod respectively.

## Main results #

• polynomial.nat_degree_prod_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.
• polynomial.nat_degree_prod : for polynomials over an integral domain, the degree of the product is the sum of degrees.
• polynomial.leading_coeff_prod : for polynomials over an integral domain, the leading coefficient is the product of leading coefficients.
• polynomial.prod_X_sub_C_coeff_card_pred carries most of the content for computing the second coefficient of the characteristic polynomial.
theorem polynomial.nat_degree_list_sum_le {α : Type u_1} [semiring α] (l : list (polynomial α)) :
theorem polynomial.nat_degree_multiset_sum_le {α : Type u_1} [semiring α] (l : multiset (polynomial α)) :
theorem polynomial.nat_degree_sum_le {ι : Type w} (s : finset ι) {α : Type u_1} [semiring α] (f : ι → ) :
(∑ (i : ι) in s, f i).nat_degree s
theorem polynomial.degree_list_sum_le {α : Type u_1} [semiring α] (l : list (polynomial α)) :
theorem polynomial.nat_degree_list_prod_le {α : Type u_1} [semiring α] (l : list (polynomial α)) :
theorem polynomial.coeff_list_prod_of_nat_degree_le {α : Type u_1} [semiring α] (l : list (polynomial α)) (n : ) (hl : ∀ (p : , p lp.nat_degree n) :
l.prod.coeff ((l.length) * n) = (list.map (λ (p : , p.coeff n) l).prod
theorem polynomial.nat_degree_prod_le {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) :
(∏ (i : ι) in s, f i).nat_degree ∑ (i : ι) in s, (f i).nat_degree
theorem polynomial.leading_coeff_multiset_prod' {R : Type u} (t : multiset (polynomial R)) (h : 0) :

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.

theorem polynomial.leading_coeff_prod' {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) (h : ∏ (i : ι) in s, (f i).leading_coeff 0) :
(∏ (i : ι) in s, f i).leading_coeff = ∏ (i : ι) in s, (f i).leading_coeff

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_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem polynomial.nat_degree_multiset_prod' {R : Type u} (t : multiset (polynomial R)) (h : (multiset.map (λ (f : , f.leading_coeff) t).prod 0) :

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.

theorem polynomial.nat_degree_prod' {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) (h : ∏ (i : ι) in s, (f i).leading_coeff 0) :
(∏ (i : ι) in s, f i).nat_degree = ∑ (i : ι) in s, (f i).nat_degree

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_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem polynomial.nat_degree_multiset_prod_of_monic {R : Type u} (t : multiset (polynomial R)) [nontrivial R] (h : ∀ (f : , f t → f.monic) :
theorem polynomial.nat_degree_prod_of_monic {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) [nontrivial R] (h : ∀ (i : ι), i s(f i).monic) :
(∏ (i : ι) in s, f i).nat_degree = ∑ (i : ι) in s, (f i).nat_degree
theorem polynomial.coeff_multiset_prod_of_nat_degree_le {R : Type u} (t : multiset (polynomial R)) (n : ) (hl : ∀ (p : , p tp.nat_degree n) :
t.prod.coeff ((multiset.card t) * n) = (multiset.map (λ (p : , p.coeff n) t).prod
theorem polynomial.coeff_prod_of_nat_degree_le {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) (n : ) (h : ∀ (p : ι), p s(f p).nat_degree n) :
(∏ (i : ι) in s, f i).coeff ((s.card) * n) = ∏ (i : ι) in s, (f i).coeff n
theorem polynomial.coeff_zero_multiset_prod {R : Type u} (t : multiset (polynomial R)) :
t.prod.coeff 0 = (multiset.map (λ (f : , f.coeff 0) t).prod
theorem polynomial.coeff_zero_prod {R : Type u} {ι : Type w} (s : finset ι) (f : ι → ) :
(∏ (i : ι) in s, f i).coeff 0 = ∏ (i : ι) in s, (f i).coeff 0
theorem polynomial.prod_X_sub_C_next_coeff {R : Type u} {ι : Type w} [comm_ring R] [nontrivial R] {s : finset ι} (f : ι → R) :
(∏ (i : ι) in s, (polynomial.X - polynomial.C (f i))).next_coeff = -∑ (i : ι) in s, f i
theorem polynomial.multiset_prod_X_sub_C_coeff_card_pred {R : Type u} [comm_ring R] [nontrivial R] (t : multiset R) (ht : 0 < ) :
(multiset.map (λ (x : R), t).prod.coeff - 1) = -t.sum
theorem polynomial.prod_X_sub_C_coeff_card_pred {R : Type u} {ι : Type w} [comm_ring R] [nontrivial R] (s : finset ι) (f : ι → R) (hs : 0 < s.card) :
(∏ (i : ι) in s, (polynomial.X - polynomial.C (f i))).coeff (s.card - 1) = -∑ (i : ι) in s, f i
theorem polynomial.nat_degree_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_ring R] (f : ι → ) [nontrivial R] (h : ∀ (i : ι), i sf i 0) :
(∏ (i : ι) in s, f i).nat_degree = ∑ (i : ι) in s, (f i).nat_degree

The degree of a product of polynomials is equal to the sum of the degrees.

See polynomial.nat_degree_prod' (with a ') for a version for commutative semirings, where additionally, the product of the leading coefficients must be nonzero.

theorem polynomial.nat_degree_multiset_prod {R : Type u} [comm_ring R] [nontrivial R] (s : multiset (polynomial R)) (h : 0 s) :
theorem polynomial.degree_multiset_prod {R : Type u} [comm_ring R] (t : multiset (polynomial R)) [nontrivial R] :
t.prod.degree = (multiset.map (λ (f : , f.degree) t).sum

The degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥.

theorem polynomial.degree_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_ring R] (f : ι → ) [nontrivial R] :
(∏ (i : ι) in s, f i).degree = ∑ (i : ι) in s, (f i).degree

The degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥.

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.

theorem polynomial.leading_coeff_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_ring R] (f : ι → ) :
(∏ (i : ι) in s, f i).leading_coeff = ∏ (i : ι) in s, (f i).leading_coeff

The leading coefficient of a product of polynomials is equal to the product of the leading coefficients.

See polynomial.leading_coeff_prod' (with a ') for a version for commutative semirings, where additionally, the product of the leading coefficients must be nonzero.