# Documentation

Mathlib.Algebra.Polynomial.BigOperators

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

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

## Main results #

• Polynomial.natDegree_prod_of_monic : the degree of a product of monic polynomials is the product of degrees. We prove this only for [CommSemiring R], but it ought to be true for [Semiring R] and List.prod.
• Polynomial.natDegree_prod : for polynomials over an integral domain, the degree of the product is the sum of degrees.
• Polynomial.leadingCoeff_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.natDegree_list_sum_le {S : Type u_1} [] (l : List ()) :
List.foldr max 0 (List.map Polynomial.natDegree l)
theorem Polynomial.natDegree_multiset_sum_le {S : Type u_1} [] (l : ) :
Multiset.foldr max (_ : ∀ (a b c : ), max a (max b c) = max b (max a c)) 0 (Multiset.map Polynomial.natDegree l)
theorem Polynomial.natDegree_sum_le {ι : Type w} (s : ) {S : Type u_1} [] (f : ι) :
Polynomial.natDegree (Finset.sum s fun i => f i) Finset.fold max 0 (Polynomial.natDegree f) s
theorem Polynomial.degree_list_sum_le {S : Type u_1} [] (l : List ()) :
List.maximum (List.map Polynomial.natDegree l)
theorem Polynomial.natDegree_list_prod_le {S : Type u_1} [] (l : List ()) :
List.sum (List.map Polynomial.natDegree l)
theorem Polynomial.degree_list_prod_le {S : Type u_1} [] (l : List ()) :
List.sum (List.map Polynomial.degree l)
theorem Polynomial.coeff_list_prod_of_natDegree_le {S : Type u_1} [] (l : List ()) (n : ) (hl : ∀ (p : ), p l) :
Polynomial.coeff () ( * n) = List.prod (List.map (fun p => ) l)
theorem Polynomial.natDegree_multiset_prod_le {R : Type u} [] (t : ) :
Multiset.sum (Multiset.map Polynomial.natDegree t)
theorem Polynomial.natDegree_prod_le {R : Type u} {ι : Type w} (s : ) [] (f : ι) :
theorem Polynomial.degree_multiset_prod_le {R : Type u} [] (t : ) :
Multiset.sum (Multiset.map Polynomial.degree t)

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

theorem Polynomial.degree_prod_le {R : Type u} {ι : Type w} (s : ) [] (f : ι) :
theorem Polynomial.leadingCoeff_multiset_prod' {R : Type u} [] (t : ) (h : Multiset.prod (Multiset.map Polynomial.leadingCoeff t) 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.leadingCoeff_multiset_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.leadingCoeff_prod' {R : Type u} {ι : Type w} (s : ) [] (f : ι) (h : (Finset.prod s fun i => ) 0) :
Polynomial.leadingCoeff (Finset.prod s fun i => f i) = Finset.prod s fun i =>

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

theorem Polynomial.natDegree_multiset_prod' {R : Type u} [] (t : ) (h : Multiset.prod (Multiset.map (fun f => ) t) 0) :
= Multiset.sum (Multiset.map (fun f => ) t)

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

theorem Polynomial.natDegree_prod' {R : Type u} {ι : Type w} (s : ) [] (f : ι) (h : (Finset.prod s fun i => ) 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.natDegree_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.natDegree_multiset_prod_of_monic {R : Type u} [] (t : ) (h : ∀ (f : ), f t) :
= Multiset.sum (Multiset.map Polynomial.natDegree t)
theorem Polynomial.natDegree_prod_of_monic {R : Type u} {ι : Type w} (s : ) [] (f : ι) (h : ∀ (i : ι), i sPolynomial.Monic (f i)) :
theorem Polynomial.coeff_multiset_prod_of_natDegree_le {R : Type u} [] (t : ) (n : ) (hl : ∀ (p : ), p t) :
Polynomial.coeff () (Multiset.card t * n) = Multiset.prod (Multiset.map (fun p => ) t)
theorem Polynomial.coeff_prod_of_natDegree_le {R : Type u} {ι : Type w} (s : ) [] (f : ι) (n : ) (h : ∀ (p : ι), p sPolynomial.natDegree (f p) n) :
Polynomial.coeff (Finset.prod s fun i => f i) ( * n) = Finset.prod s fun i => Polynomial.coeff (f i) n
theorem Polynomial.coeff_zero_multiset_prod {R : Type u} [] (t : ) :
= Multiset.prod (Multiset.map (fun f => ) t)
theorem Polynomial.coeff_zero_prod {R : Type u} {ι : Type w} (s : ) [] (f : ι) :
Polynomial.coeff (Finset.prod s fun i => f i) 0 = Finset.prod s fun i => Polynomial.coeff (f i) 0
theorem Polynomial.multiset_prod_X_sub_C_nextCoeff {R : Type u} [] (t : ) :
Polynomial.nextCoeff (Multiset.prod (Multiset.map (fun x => Polynomial.X - Polynomial.C x) t)) =
theorem Polynomial.prod_X_sub_C_nextCoeff {R : Type u} {ι : Type w} [] {s : } (f : ιR) :
Polynomial.nextCoeff (Finset.prod s fun i => Polynomial.X - Polynomial.C (f i)) = -Finset.sum s fun i => f i
theorem Polynomial.multiset_prod_X_sub_C_coeff_card_pred {R : Type u} [] (t : ) (ht : 0 < Multiset.card t) :
Polynomial.coeff (Multiset.prod (Multiset.map (fun x => Polynomial.X - Polynomial.C x) t)) (Multiset.card t - 1) =
theorem Polynomial.prod_X_sub_C_coeff_card_pred {R : Type u} {ι : Type w} [] (s : ) (f : ιR) (hs : 0 < ) :
Polynomial.coeff (Finset.prod s fun i => Polynomial.X - Polynomial.C (f i)) ( - 1) = -Finset.sum s fun i => f i
theorem Polynomial.degree_list_prod {R : Type u} [] [] [] (l : List ()) :
= List.sum (List.map Polynomial.degree l)

The degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥. [Nontrivial R] is needed, otherwise for l = [] we have ⊥ in the LHS and 0 in the RHS.

theorem Polynomial.natDegree_prod {R : Type u} {ι : Type w} (s : ) [] [] (f : ι) (h : ∀ (i : ι), i sf i 0) :

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

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

theorem Polynomial.natDegree_multiset_prod {R : Type u} [] [] (t : ) (h : ¬0 t) :
= Multiset.sum (Multiset.map Polynomial.natDegree t)
theorem Polynomial.degree_multiset_prod {R : Type u} [] [] (t : ) [] :
= Multiset.sum (Multiset.map (fun f => ) t)

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 : ) [] [] (f : ι) [] :
Polynomial.degree (Finset.prod s fun i => f i) = Finset.sum s fun i => Polynomial.degree (f i)

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.leadingCoeff_multiset_prod {R : Type u} [] [] (t : ) :
= Multiset.prod (Multiset.map (fun f => ) t)

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

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

theorem Polynomial.leadingCoeff_prod {R : Type u} {ι : Type w} (s : ) [] [] (f : ι) :
Polynomial.leadingCoeff (Finset.prod s fun i => f i) = Finset.prod s fun i =>

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

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