Polynomials
Lemmas for the interaction between polynomials and ∑ and ∏.
Main results
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.nat_degree_prod: for polynomials over an integral domain, the degree of the product is the sum of degreesleading_coeff_prod: for polynomials over an integral domain, the leading coefficient is the product of leading coefficientsprod_X_sub_C_coeff_card_predcarries most of the content for computing the second coefficient of the characteristic polynomial.
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.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 ∈ s → f 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