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)) : l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

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

theorem Polynomial.natDegree_sum_le {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] (f : ι → Polynomial S) : (∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (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, (f i).natDegree ≤ n) : (∑ i ∈ s, f i).natDegree ≤ n

theorem Polynomial.leadingCoeff_sum_of_degree_eq {ι : Type w} {S : Type u_1} [Semiring S] {f : ι → Polynomial S} {s : Finset ι} {d : WithBot ℕ} (hd : ∀ k ∈ s, (f k).degree = d) (hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0) : (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

The leading coefficient of a sum of polynomials with the same degree is the sum of the leading coefficients, provided that this sum is nonzero.

theorem Polynomial.degree_list_sum_le_of_forall_degree_le {S : Type u_1} [Semiring S] (l : List (Polynomial S)) (n : WithBot ℕ) (hl : ∀ p ∈ l, p.degree ≤ n) : l.sum.degree ≤ n

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

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

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

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

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

theorem Polynomial.natDegree_prod_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) : (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree

theorem Polynomial.degree_multiset_prod_le {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) : t.prod.degree ≤ (Multiset.map 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 ⊥.

theorem Polynomial.degree_prod_le {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) : (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

theorem Polynomial.leadingCoeff_multiset_prod' {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : (Multiset.map leadingCoeff t).prod ≠ 0) : t.prod.leadingCoeff = (Multiset.map leadingCoeff 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.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 : ∏ i ∈ s, (f i).leadingCoeff ≠ 0) : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

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.map (fun (f : Polynomial R) => f.leadingCoeff) t).prod ≠ 0) : t.prod.natDegree = (Multiset.map (fun (f : Polynomial R) => f.natDegree) 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.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 : ∏ i ∈ s, (f i).leadingCoeff ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

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, f.Monic) : t.prod.natDegree = (Multiset.map natDegree t).sum

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

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

theorem Polynomial.degree_prod_of_monic {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

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

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

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

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

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

theorem Polynomial.prod_X_sub_C_nextCoeff {R : Type u} {ι : Type w} [CommRing R] {s : Finset ι} (f : ι → R) : (∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i

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

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

theorem Polynomial.degree_sum_eq_of_linearIndepOn {R : Type u} {ι : Type w} (s : Finset ι) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] {f : ι → Polynomial R} {v : ι → A} (h : LinearIndepOn R v ↑s) : (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree = s.sup fun (i : ι) => (f i).degree

theorem Polynomial.natDegree_sum_eq_of_linearIndepOn {R : Type u} {ι : Type w} (s : Finset ι) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] {f : ι → Polynomial R} {v : ι → A} (h : LinearIndepOn R v ↑s) : (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree = s.sup fun (i : ι) => (f i).natDegree

@[simp]

theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [CommRing R] [Nontrivial R] (s : Multiset R) : (Multiset.map (fun (x : R) => X - C x) s).prod.natDegree = s.card

@[simp]

theorem Polynomial.natDegree_finset_prod_X_sub_C_eq_card {R : Type u} [CommRing R] [Nontrivial R] {α : Type u_1} (s : Finset α) (f : α → R) : (∏ a ∈ s, (X - C (f a))).natDegree = s.card

theorem Polynomial.degree_list_prod {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (l : List (Polynomial R)) : l.prod.degree = (List.map 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.

theorem Polynomial.natDegree_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) (h : ∀ i ∈ s, f i ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

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) : t.prod.natDegree = (Multiset.map natDegree t).sum

theorem Polynomial.degree_multiset_prod {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) [Nontrivial R] : t.prod.degree = (Multiset.map (fun (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 ⊥.

theorem Polynomial.degree_prod {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) [Nontrivial R] : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (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 ⊥.

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

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) : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

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.