Lemmas for the interaction between polynomials and ∑ and ∏.

Recall that ∑ and ∏ are notation for Finset.sum and Finset.prod respectively.

Main results

• Polynomial.natDegree_prod_of_monic : the degree of a product of monic polynomials is the product of degrees. We prove this only for [CommSemiring R], but it ought to be true for [Semiring R] and List.prod.
• Polynomial.natDegree_prod : for polynomials over an integral domain, the degree of the product is the sum of degrees.
• Polynomial.leadingCoeff_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.

theorem Polynomial.natDegree_list_sum_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : Polynomial.natDegree (List.sum l) ≤ List.foldr max 0 (List.map Polynomial.natDegree l)

theorem Polynomial.natDegree_multiset_sum_le {S : Type u_1} [Semiring S] (l : Multiset (Polynomial S)) : Polynomial.natDegree (Multiset.sum l) ≤ Multiset.foldr max ⋯ 0 (Multiset.map Polynomial.natDegree l)

theorem Polynomial.natDegree_sum_le {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] (f : ι → Polynomial S) : Polynomial.natDegree (Finset.sum s fun (i : ι) => f i) ≤ Finset.fold max 0 (Polynomial.natDegree ∘ f) s

theorem Polynomial.natDegree_sum_le_of_forall_le {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] {n : ℕ} (f : ι → Polynomial S) (h : ∀ i ∈ s, Polynomial.natDegree (f i) ≤ n) : Polynomial.natDegree (Finset.sum s fun (i : ι) => f i) ≤ n

theorem Polynomial.degree_list_sum_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : Polynomial.degree (List.sum l) ≤ List.maximum (List.map Polynomial.natDegree l)

theorem Polynomial.natDegree_list_prod_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : Polynomial.natDegree (List.prod l) ≤ List.sum (List.map Polynomial.natDegree l)

theorem Polynomial.degree_list_prod_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : Polynomial.degree (List.prod l) ≤ List.sum (List.map Polynomial.degree l)

theorem Polynomial.coeff_list_prod_of_natDegree_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) (n : ℕ) (hl : ∀ p ∈ l, Polynomial.natDegree p ≤ n) : Polynomial.coeff (List.prod l) (List.length l * n) = List.prod (List.map (fun (p : Polynomial S) => Polynomial.coeff p n) l)

theorem Polynomial.natDegree_multiset_prod_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) : Polynomial.natDegree (Multiset.prod t) ≤ Multiset.sum (Multiset.map Polynomial.natDegree t)

theorem Polynomial.natDegree_prod_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) : Polynomial.natDegree (Finset.prod s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => Polynomial.natDegree (f i)

theorem Polynomial.degree_multiset_prod_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) : Polynomial.degree (Multiset.prod t) ≤ Multiset.sum (Multiset.map Polynomial.degree t)

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 ι) [CommSemiring R] (f : ι → Polynomial R) : Polynomial.degree (Finset.prod s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => Polynomial.degree (f i)

theorem Polynomial.leadingCoeff_multiset_prod' {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : Multiset.prod (Multiset.map Polynomial.leadingCoeff t) ≠ 0) : Polynomial.leadingCoeff (Multiset.prod t) = Multiset.prod (Multiset.map Polynomial.leadingCoeff t)

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.leadingCoeff_multiset_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.leadingCoeff_prod' {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : (Finset.prod s fun (i : ι) => Polynomial.leadingCoeff (f i)) ≠ 0) : Polynomial.leadingCoeff (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => Polynomial.leadingCoeff (f i)

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.leadingCoeff_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.natDegree_multiset_prod' {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : Multiset.prod (Multiset.map (fun (f : Polynomial R) => Polynomial.leadingCoeff f) t) ≠ 0) : Polynomial.natDegree (Multiset.prod t) = Multiset.sum (Multiset.map (fun (f : Polynomial R) => Polynomial.natDegree f) t)

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.natDegree_multiset_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.natDegree_prod' {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : (Finset.prod s fun (i : ι) => Polynomial.leadingCoeff (f i)) ≠ 0) : Polynomial.natDegree (Finset.prod s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Polynomial.natDegree (f i)

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.natDegree_prod (without the ') for a version for integral domains, where this condition is automatically satisfied.

theorem Polynomial.natDegree_multiset_prod_of_monic {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : ∀ f ∈ t, Polynomial.Monic f) : Polynomial.natDegree (Multiset.prod t) = Multiset.sum (Multiset.map Polynomial.natDegree t)

theorem Polynomial.natDegree_prod_of_monic {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : ∀ i ∈ s, Polynomial.Monic (f i)) : Polynomial.natDegree (Finset.prod s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Polynomial.natDegree (f i)

theorem Polynomial.coeff_multiset_prod_of_natDegree_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (n : ℕ) (hl : ∀ p ∈ t, Polynomial.natDegree p ≤ n) : Polynomial.coeff (Multiset.prod t) (Multiset.card t * n) = Multiset.prod (Multiset.map (fun (p : Polynomial R) => Polynomial.coeff p n) t)

theorem Polynomial.coeff_prod_of_natDegree_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (n : ℕ) (h : ∀ p ∈ s, Polynomial.natDegree (f p) ≤ n) : Polynomial.coeff (Finset.prod s fun (i : ι) => f i) (s.card * n) = Finset.prod s fun (i : ι) => Polynomial.coeff (f i) n

theorem Polynomial.coeff_zero_multiset_prod {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) : Polynomial.coeff (Multiset.prod t) 0 = Multiset.prod (Multiset.map (fun (f : Polynomial R) => Polynomial.coeff f 0) t)

theorem Polynomial.coeff_zero_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) : Polynomial.coeff (Finset.prod s fun (i : ι) => f i) 0 = Finset.prod s fun (i : ι) => Polynomial.coeff (f i) 0

theorem Polynomial.multiset_prod_X_sub_C_nextCoeff {R : Type u} [CommRing R] (t : Multiset R) : Polynomial.nextCoeff (Multiset.prod (Multiset.map (fun (x : R) => Polynomial.X - Polynomial.C x) t)) = -Multiset.sum t

theorem Polynomial.prod_X_sub_C_nextCoeff {R : Type u} {ι : Type w} [CommRing R] {s : Finset ι} (f : ι → R) : Polynomial.nextCoeff (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i)) = -Finset.sum s fun (i : ι) => f i

theorem Polynomial.multiset_prod_X_sub_C_coeff_card_pred {R : Type u} [CommRing R] (t : Multiset R) (ht : 0 < Multiset.card t) : Polynomial.coeff (Multiset.prod (Multiset.map (fun (x : R) => Polynomial.X - Polynomial.C x) t)) (Multiset.card t - 1) = -Multiset.sum t

theorem Polynomial.prod_X_sub_C_coeff_card_pred {R : Type u} {ι : Type w} [CommRing R] (s : Finset ι) (f : ι → R) (hs : 0 < s.card) : Polynomial.coeff (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i)) (s.card - 1) = -Finset.sum s fun (i : ι) => f i

theorem Polynomial.degree_list_prod {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (l : List (Polynomial R)) : Polynomial.degree (List.prod l) = List.sum (List.map Polynomial.degree l)

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.natDegree_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) (h : ∀ i ∈ s, f i ≠ 0) : Polynomial.natDegree (Finset.prod s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Polynomial.natDegree (f i)

The degree of a product of polynomials is equal to the sum of the degrees.

See Polynomial.natDegree_prod' (with a ') for a version for commutative semirings, where additionally, the product of the leading coefficients must be nonzero.

theorem Polynomial.natDegree_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) (h : 0 ∉ t) : Polynomial.natDegree (Multiset.prod t) = Multiset.sum (Multiset.map Polynomial.natDegree t)

theorem Polynomial.degree_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) [Nontrivial R] : Polynomial.degree (Multiset.prod t) = Multiset.sum (Multiset.map (fun (f : Polynomial R) => Polynomial.degree f) t)

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 ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) [Nontrivial R] : Polynomial.degree (Finset.prod s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Polynomial.degree (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 ⊥.

theorem Polynomial.leadingCoeff_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) : Polynomial.leadingCoeff (Multiset.prod t) = Multiset.prod (Multiset.map (fun (f : Polynomial R) => Polynomial.leadingCoeff f) t)

The leading coefficient of a product of polynomials is equal to the product of the leading coefficients.

See Polynomial.leadingCoeff_multiset_prod' (with a ') for a version for commutative semirings, where additionally, the product of the leading coefficients must be nonzero.

theorem Polynomial.leadingCoeff_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) : Polynomial.leadingCoeff (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => Polynomial.leadingCoeff (f i)

The leading coefficient of a product of polynomials is equal to the product of the leading coefficients.

See Polynomial.leadingCoeff_prod' (with a ') for a version for commutative semirings, where additionally, the product of the leading coefficients must be nonzero.