mathlib documentation

algebra.polynomial.big_operators

Polynomials

Lemmas for the interaction between polynomials and ∑ and ∏.

Main results

theorem polynomial.nat_degree_prod_le {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι → polynomial R) :
(∏ (i : ι) in s, f i).nat_degree ∑ (i : ι) in s, (f i).nat_degree

theorem polynomial.leading_coeff_prod' {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι → polynomial R) (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 leading_coeff_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 : ∏ (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 product of the degrees, provided that the product of leading coefficients is nonzero.

See 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) [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_zero_prod {R : Type u} {ι : Type w} (s : finset ι) [comm_semiring R] (f : ι → polynomial R) :
(∏ (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.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 ι) [integral_domain R] (f : ι → polynomial R) (h : ∀ (i : ι), i sf i 0) :
(∏ (i : ι) in s, f i).nat_degree = ∑ (i : ι) in s, (f i).nat_degree

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