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) :
(s.prod (λ (i : ι), f i)).nat_degree ≤ s.sum (λ (i : ι), (f i).nat_degree)
theorem
polynomial.leading_coeff_prod'
{R : Type u}
{ι : Type w}
(s : finset ι)
[comm_semiring R]
(f : ι → polynomial R) :
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 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) :
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 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] :
(∀ (i : ι), i ∈ s → (f i).monic) → (s.prod (λ (i : ι), f i)).nat_degree = s.sum (λ (i : ι), (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) :
(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]
[nontrivial R]
(s : finset ι)
(f : ι → R) :
theorem
polynomial.nat_degree_prod
{R : Type u}
{ι : Type w}
(s : finset ι)
[integral_domain R]
(f : ι → polynomial R) :
(∀ (i : ι), i ∈ s → f i ≠ 0) → (s.prod (λ (i : ι), f i)).nat_degree = s.sum (λ (i : ι), (f i).nat_degree)
theorem
polynomial.leading_coeff_prod
{R : Type u}
{ι : Type w}
(s : finset ι)
[integral_domain R]
(f : ι → polynomial R) :
(s.prod (λ (i : ι), f i)).leading_coeff = s.prod (λ (i : ι), (f i).leading_coeff)