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 #

theorem Polynomial.natDegree_list_sum_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
l.sum.natDegree List.foldr max 0 (List.map Polynomial.natDegree l)
theorem Polynomial.natDegree_multiset_sum_le {S : Type u_1} [Semiring S] (l : Multiset (Polynomial S)) :
l.sum.natDegree Multiset.foldr max 0 (Multiset.map Polynomial.natDegree l)
theorem Polynomial.natDegree_sum_le {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] (f : ιPolynomial S) :
(is, f i).natDegree Finset.fold max 0 (Polynomial.natDegree f) s
theorem Polynomial.natDegree_sum_le_of_forall_le {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] {n : } (f : ιPolynomial S) (h : is, (f i).natDegree n) :
(is, f i).natDegree n
theorem Polynomial.degree_list_sum_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
l.sum.degree (List.map Polynomial.natDegree l).maximum
theorem Polynomial.natDegree_list_prod_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
l.prod.natDegree (List.map Polynomial.natDegree l).sum
theorem Polynomial.degree_list_prod_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
l.prod.degree (List.map Polynomial.degree l).sum
theorem Polynomial.coeff_list_prod_of_natDegree_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) (n : ) (hl : pl, p.natDegree n) :
l.prod.coeff (l.length * n) = (List.map (fun (p : Polynomial S) => p.coeff n) l).prod
theorem Polynomial.natDegree_multiset_prod_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) :
t.prod.natDegree (Multiset.map Polynomial.natDegree t).sum
theorem Polynomial.natDegree_prod_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ιPolynomial R) :
(is, f i).natDegree is, (f i).natDegree
theorem Polynomial.degree_multiset_prod_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) :
t.prod.degree (Multiset.map Polynomial.degree t).sum

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 : Finset ι) [CommSemiring R] (f : ιPolynomial R) :
(is, f i).degree is, (f i).degree
theorem Polynomial.leadingCoeff_multiset_prod' {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : (Multiset.map Polynomial.leadingCoeff t).prod 0) :
t.prod.leadingCoeff = (Multiset.map Polynomial.leadingCoeff t).prod

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 : Finset ι) [CommSemiring R] (f : ιPolynomial R) (h : is, (f i).leadingCoeff 0) :
(is, f i).leadingCoeff = is, (f i).leadingCoeff

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} [CommSemiring R] (t : Multiset (Polynomial R)) (h : (Multiset.map (fun (f : Polynomial R) => f.leadingCoeff) t).prod 0) :
t.prod.natDegree = (Multiset.map (fun (f : Polynomial R) => f.natDegree) t).sum

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 : Finset ι) [CommSemiring R] (f : ιPolynomial R) (h : is, (f i).leadingCoeff 0) :
(is, f i).natDegree = is, (f i).natDegree

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} [CommSemiring R] (t : Multiset (Polynomial R)) (h : ft, f.Monic) :
t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
theorem Polynomial.natDegree_prod_of_monic {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ιPolynomial R) (h : is, (f i).Monic) :
(is, f i).natDegree = is, (f i).natDegree
theorem Polynomial.coeff_multiset_prod_of_natDegree_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (n : ) (hl : pt, p.natDegree n) :
t.prod.coeff (Multiset.card t * n) = (Multiset.map (fun (p : Polynomial R) => p.coeff n) t).prod
theorem Polynomial.coeff_prod_of_natDegree_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ιPolynomial R) (n : ) (h : ps, (f p).natDegree n) :
(is, f i).coeff (s.card * n) = is, (f i).coeff n
theorem Polynomial.coeff_zero_multiset_prod {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) :
t.prod.coeff 0 = (Multiset.map (fun (f : Polynomial R) => f.coeff 0) t).prod
theorem Polynomial.coeff_zero_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ιPolynomial R) :
(is, f i).coeff 0 = is, (f i).coeff 0
theorem Polynomial.multiset_prod_X_sub_C_nextCoeff {R : Type u} [CommRing R] (t : Multiset R) :
(Multiset.map (fun (x : R) => Polynomial.X - Polynomial.C x) t).prod.nextCoeff = -t.sum
theorem Polynomial.prod_X_sub_C_nextCoeff {R : Type u} {ι : Type w} [CommRing R] {s : Finset ι} (f : ιR) :
(is, (Polynomial.X - Polynomial.C (f i))).nextCoeff = -is, f i
theorem Polynomial.multiset_prod_X_sub_C_coeff_card_pred {R : Type u} [CommRing R] (t : Multiset R) (ht : 0 < Multiset.card t) :
(Multiset.map (fun (x : R) => Polynomial.X - Polynomial.C x) t).prod.coeff (Multiset.card t - 1) = -t.sum
theorem Polynomial.prod_X_sub_C_coeff_card_pred {R : Type u} {ι : Type w} [CommRing R] (s : Finset ι) (f : ιR) (hs : 0 < s.card) :
(is, (Polynomial.X - Polynomial.C (f i))).coeff (s.card - 1) = -is, f i
theorem Polynomial.degree_list_prod {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (l : List (Polynomial R)) :
l.prod.degree = (List.map Polynomial.degree l).sum

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 : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ιPolynomial R) (h : is, f i 0) :
(is, f i).natDegree = is, (f i).natDegree

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} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) (h : 0t) :
t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
theorem Polynomial.degree_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) [Nontrivial R] :
t.prod.degree = (Multiset.map (fun (f : Polynomial R) => 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 ι) [CommSemiring R] [NoZeroDivisors R] (f : ιPolynomial R) [Nontrivial R] :
(is, f i).degree = is, (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 ⊥.

theorem Polynomial.leadingCoeff_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) :
t.prod.leadingCoeff = (Multiset.map (fun (f : Polynomial R) => f.leadingCoeff) t).prod

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 : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ιPolynomial R) :
(is, f i).leadingCoeff = is, (f i).leadingCoeff

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.