mathlib3 documentation

algebra.polynomial.big_operators

Lemmas for the interaction between polynomials and and . #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

theorem polynomial.nat_degree_sum_le {ι : Type w} (s : finset ι) {S : Type u_1} [semiring S] (f : ι polynomial S) :
theorem polynomial.coeff_list_prod_of_nat_degree_le {S : Type u_1} [semiring S] (l : list (polynomial S)) (n : ) (hl : (p : polynomial S), p l p.nat_degree n) :
l.prod.coeff (l.length * n) = (list.map (λ (p : polynomial S), p.coeff n) l).prod
theorem polynomial.nat_degree_prod_le {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι polynomial R) :
(s.prod (λ (i : ι), f i)).nat_degree s.sum (λ (i : ι), (f i).nat_degree)

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 ι) [comm_semiring R] (f : ι polynomial R) :
(s.prod (λ (i : ι), f i)).degree s.sum (λ (i : ι), (f i).degree)

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 ι) [comm_semiring R] (f : ι polynomial R) (h : s.prod (λ (i : ι), (f i).leading_coeff) 0) :
(s.prod (λ (i : ι), f i)).leading_coeff = s.prod (λ (i : ι), (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.

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 ι) [comm_semiring R] (f : ι polynomial R) (h : s.prod (λ (i : ι), (f i).leading_coeff) 0) :
(s.prod (λ (i : ι), f i)).nat_degree = s.sum (λ (i : ι), (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_prod_of_monic {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι polynomial R) (h : (i : ι), i s (f i).monic) :
(s.prod (λ (i : ι), f i)).nat_degree = s.sum (λ (i : ι), (f i).nat_degree)
theorem polynomial.coeff_prod_of_nat_degree_le {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι polynomial R) (n : ) (h : (p : ι), p s (f p).nat_degree n) :
(s.prod (λ (i : ι), f i)).coeff (s.card * n) = s.prod (λ (i : ι), (f i).coeff n)
theorem polynomial.coeff_zero_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι polynomial R) :
(s.prod (λ (i : ι), f i)).coeff 0 = s.prod (λ (i : ι), (f i).coeff 0)
theorem polynomial.prod_X_sub_C_next_coeff {R : Type u} {ι : Type w} [comm_ring R] {s : finset ι} (f : ι R) :
(s.prod (λ (i : ι), polynomial.X - polynomial.C (f i))).next_coeff = -s.sum (λ (i : ι), f i)
theorem polynomial.prod_X_sub_C_coeff_card_pred {R : Type u} {ι : Type w} [comm_ring R] (s : finset ι) (f : ι R) (hs : 0 < s.card) :
(s.prod (λ (i : ι), polynomial.X - polynomial.C (f i))).coeff (s.card - 1) = -s.sum (λ (i : ι), 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 ⊥. [nontrivial R] is needed, otherwise for l = [] we have in the LHS and 0 in the RHS.

theorem polynomial.nat_degree_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] [no_zero_divisors R] (f : ι polynomial R) (h : (i : ι), i s f i 0) :
(s.prod (λ (i : ι), f i)).nat_degree = s.sum (λ (i : ι), (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.

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_semiring R] [no_zero_divisors R] (f : ι polynomial R) [nontrivial R] :
(s.prod (λ (i : ι), f i)).degree = s.sum (λ (i : ι), (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_semiring R] [no_zero_divisors R] (f : ι polynomial R) :
(s.prod (λ (i : ι), f i)).leading_coeff = s.prod (λ (i : ι), (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.