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 #

polynomial.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.
polynomial.nat_degree_prod : for polynomials over an integral domain, the degree of the product is the sum of degrees.
polynomial.leading_coeff_prod : for polynomials over an integral domain, the leading coefficient is the product of leading coefficients.
polynomial.prod_X_sub_C_coeff_card_pred carries most of the content for computing the second coefficient of the characteristic polynomial.

source

theorem polynomial.nat_degree_list_sum_le {S : Type u_1} [semiring S] (l : list (polynomial S)) :

l.sum.nat_degree ≤ list.foldr linear_order.max 0 (list.map polynomial.nat_degree l)

source

theorem polynomial.nat_degree_multiset_sum_le {S : Type u_1} [semiring S] (l : multiset (polynomial S)) :

l.sum.nat_degree ≤ multiset.foldr linear_order.max max_left_comm 0 (multiset.map polynomial.nat_degree l)

source

theorem polynomial.nat_degree_sum_le {ι : Type w} (s : finset ι) {S : Type u_1} [semiring S] (f : ι → polynomial S) :

(s.sum (λ (i : ι), f i)).nat_degree ≤ finset.fold linear_order.max 0 (polynomial.nat_degree ∘ f) s

source

theorem polynomial.degree_list_sum_le {S : Type u_1} [semiring S] (l : list (polynomial S)) :

l.sum.degree ≤ (list.map polynomial.nat_degree l).maximum

source

theorem polynomial.nat_degree_list_prod_le {S : Type u_1} [semiring S] (l : list (polynomial S)) :

l.prod.nat_degree ≤ (list.map polynomial.nat_degree l).sum

source

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

source

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

source

theorem polynomial.nat_degree_multiset_prod_le {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) :

t.prod.nat_degree ≤ (multiset.map polynomial.nat_degree t).sum

source

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)

source

theorem polynomial.degree_multiset_prod_le {R : Type u} [comm_semiring 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 ⊥.

source

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)

source

theorem polynomial.leading_coeff_multiset_prod' {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) (h : (multiset.map polynomial.leading_coeff t).prod ≠ 0) :

t.prod.leading_coeff = (multiset.map polynomial.leading_coeff 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.leading_coeff_multiset_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

source

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.

source

theorem polynomial.nat_degree_multiset_prod' {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) (h : (multiset.map (λ (f : polynomial R), f.leading_coeff) t).prod ≠ 0) :

t.prod.nat_degree = (multiset.map (λ (f : polynomial R), f.nat_degree) 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.nat_degree_multiset_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

source

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.

source

theorem polynomial.nat_degree_multiset_prod_of_monic {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) (h : ∀ (f : polynomial R), f ∈ t → f.monic) :

t.prod.nat_degree = (multiset.map polynomial.nat_degree t).sum

source

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)

source

theorem polynomial.coeff_multiset_prod_of_nat_degree_le {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) (n : ℕ) (hl : ∀ (p : polynomial R), p ∈ t → p.nat_degree ≤ n) :

t.prod.coeff (⇑multiset.card t * n) = (multiset.map (λ (p : polynomial R), p.coeff n) t).prod

source

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)

source

theorem polynomial.coeff_zero_multiset_prod {R : Type u} [comm_semiring R] (t : multiset (polynomial R)) :

t.prod.coeff 0 = (multiset.map (λ (f : polynomial R), f.coeff 0) t).prod

source

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)

source

theorem polynomial.multiset_prod_X_sub_C_next_coeff {R : Type u} [comm_ring R] (t : multiset R) :

(multiset.map (λ (x : R), polynomial.X - ⇑polynomial.C x) t).prod.next_coeff = -t.sum

source

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)

source

theorem polynomial.multiset_prod_X_sub_C_coeff_card_pred {R : Type u} [comm_ring R] (t : multiset R) (ht : 0 < ⇑multiset.card t) :

(multiset.map (λ (x : R), polynomial.X - ⇑polynomial.C x) t).prod.coeff (⇑multiset.card t - 1) = -t.sum

source

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)

source

theorem polynomial.degree_list_prod {R : Type u} [semiring R] [no_zero_divisors 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.

source

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.

source

theorem polynomial.nat_degree_multiset_prod {R : Type u} [comm_semiring R] [no_zero_divisors R] (t : multiset (polynomial R)) (h : 0 ∉ t) :

t.prod.nat_degree = (multiset.map polynomial.nat_degree t).sum

source

theorem polynomial.degree_multiset_prod {R : Type u} [comm_semiring R] [no_zero_divisors R] (t : multiset (polynomial R)) [nontrivial R] :

t.prod.degree = (multiset.map (λ (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 ⊥.

source

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 ⊥.

source

theorem polynomial.leading_coeff_multiset_prod {R : Type u} [comm_semiring R] [no_zero_divisors R] (t : multiset (polynomial R)) :

t.prod.leading_coeff = (multiset.map (λ (f : polynomial R), f.leading_coeff) t).prod

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.

source

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.

Lemmas for the interaction between polynomials and ∑ and ∏. #

Main results #

Lemmas for the interaction between polynomials and `∑` and `∏`. #