Mathlib.Algebra.Polynomial.BigOperators

Polynomial.natDegree_list_sum_le theorem

(l : List S[X]) : natDegree l.sum ≤ (l.map natDegree).foldr max 0

Full source

theorem natDegree_list_sum_le (l : List S[X]) :
    natDegree l.sum ≤ (l.map natDegree).foldr max 0 := by
  apply List.sum_le_foldr_max natDegree
  · simp
  · exact natDegree_add_le

Degree Bound for Sum of Polynomials in a List: $\text{natDegree}(\sum p) \leq \max \text{natDegree}(p)$

Informal description

For any list $l$ of univariate polynomials over a semiring $S$, the degree of the sum of the polynomials in $l$ is bounded above by the maximum degree among the polynomials in $l$, i.e., \[ \text{natDegree}\left(\sum_{p \in l} p\right) \leq \max_{p \in l} \text{natDegree}(p). \]

Polynomial.natDegree_multiset_sum_le theorem

(l : Multiset S[X]) : natDegree l.sum ≤ (l.map natDegree).foldr max 0

Full source

theorem natDegree_multiset_sum_le (l : Multiset S[X]) :
    natDegree l.sum ≤ (l.map natDegree).foldr max 0 :=
  Quotient.inductionOn l (by simpa using natDegree_list_sum_le)

Degree Bound for Sum of Polynomials in a Multiset: $\text{natDegree}(\sum p) \leq \max \text{natDegree}(p)$

Informal description

For any multiset $l$ of univariate polynomials over a semiring $S$, the degree of the sum of the polynomials in $l$ is bounded above by the maximum degree among the polynomials in $l$, i.e., \[ \text{natDegree}\left(\sum_{p \in l} p\right) \leq \max_{p \in l} \text{natDegree}(p). \]

Polynomial.natDegree_sum_le theorem

(f : ι → S[X]) : natDegree (∑ i ∈ s, f i) ≤ s.fold max 0 (natDegree ∘ f)

Full source

theorem natDegree_sum_le (f : ι → S[X]) :
    natDegree (∑ i ∈ s, f i) ≤ s.fold max 0 (natDegreenatDegree ∘ f) := by
  simpa using natDegree_multiset_sum_le (s.val.map f)

Degree Bound for Sum of Polynomials over a Finite Set: $\text{natDegree}(\sum f_i) \leq \max \text{natDegree}(f_i)$

Informal description

For any finite set $s$ and any family of univariate polynomials $f_i$ over a semiring $S$ indexed by $i \in s$, the degree of the sum $\sum_{i \in s} f_i$ is bounded above by the maximum degree among the polynomials $f_i$, i.e., \[ \text{natDegree}\left(\sum_{i \in s} f_i\right) \leq \max_{i \in s} \text{natDegree}(f_i). \]

Polynomial.natDegree_sum_le_of_forall_le theorem

{n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) : natDegree (∑ i ∈ s, f i) ≤ n

Full source

lemma natDegree_sum_le_of_forall_le {n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) :
    natDegree (∑ i ∈ s, f i) ≤ n :=
  le_trans (natDegree_sum_le s f) <| (Finset.fold_max_le n).mpr <| by simpa

Degree Bound Preservation for Sum of Polynomials with Uniform Degree Bound

Informal description

For any finite set $s$, any family of univariate polynomials $f_i$ over a semiring $S$ indexed by $i \in s$, and any natural number $n$, if each polynomial $f_i$ satisfies $\mathrm{natDegree}(f_i) \leq n$, then the sum $\sum_{i \in s} f_i$ satisfies $\mathrm{natDegree}(\sum_{i \in s} f_i) \leq n$.

Polynomial.degree_list_sum_le_of_forall_degree_le theorem

(l : List S[X]) (n : WithBot ℕ) (hl : ∀ p ∈ l, degree p ≤ n) : degree l.sum ≤ n

Full source

theorem degree_list_sum_le_of_forall_degree_le (l : List S[X])
    (n : WithBot ℕ) (hl : ∀ p ∈ l, degree p ≤ n) :
    degree l.sum ≤ n := by
  induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [List.mem_cons, forall_eq_or_imp] at hl
    rcases hl with ⟨hhd, htl⟩
    rw [List.sum_cons]
    exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

Degree Bound Preservation under Polynomial Summation

Informal description

For any list $l$ of univariate polynomials over a semiring $S$ and any extended natural number $n \in \mathbb{N} \cup \{\bot\}$, if every polynomial $p$ in $l$ satisfies $\mathrm{degree}(p) \leq n$, then the degree of the sum of polynomials in $l$ is also bounded by $n$, i.e., $\mathrm{degree}(\sum_{p \in l} p) \leq n$.

Polynomial.degree_list_sum_le theorem

(l : List S[X]) : degree l.sum ≤ (l.map natDegree).maximum

Full source

theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).maximum := by
  apply degree_list_sum_le_of_forall_degree_le
  intros p hp
  by_cases h : p = 0
  · subst h
    simp
  · rw [degree_eq_natDegree h]
    apply List.le_maximum_of_mem'
    rw [List.mem_map]
    use p
    simp [hp]

Degree Bound for Sum of Polynomials: $\deg(\sum p) \leq \max(\mathrm{natDegree}(p))$

Informal description

For any list $l$ of univariate polynomials over a semiring $S$, the degree of the sum of polynomials in $l$ is bounded above by the maximum of their natural degrees, i.e., \[ \deg\left(\sum_{p \in l} p\right) \leq \max_{p \in l} \mathrm{natDegree}(p). \]

Polynomial.natDegree_list_prod_le theorem

(l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum

Full source

theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum := by
  induction' l with hd tl IH
  · simp
  · simpa using natDegree_mul_le.trans (add_le_add_left IH _)

Upper Bound on Natural Degree of Polynomial Product

Informal description

For any list $l$ of univariate polynomials over a semiring $S$, the natural degree of the product of polynomials in $l$ is less than or equal to the sum of the natural degrees of the polynomials in $l$. That is, $\mathrm{natDegree}(\prod_{p \in l} p) \leq \sum_{p \in l} \mathrm{natDegree}(p)$.

Polynomial.degree_list_prod_le theorem

(l : List S[X]) : degree l.prod ≤ (l.map degree).sum

Full source

theorem degree_list_prod_le (l : List S[X]) : degree l.prod ≤ (l.map degree).sum := by
  induction' l with hd tl IH
  · simp
  · simpa using (degree_mul_le _ _).trans (add_le_add_left IH _)

Degree Bound for Product of Polynomials in a List

Informal description

For any list $l$ of univariate polynomials over a semiring $S$, the degree of the product of the polynomials in $l$ is less than or equal to the sum of the degrees of the individual polynomials in $l$.

Polynomial.coeff_list_prod_of_natDegree_le theorem

 (l : List S[X]) (n : ℕ) (hl : ∀ p ∈ l, natDegree p ≤ n) :
  coeff (List.prod l) (l.length * n) = (l.map fun p => coeff p n).prod

Full source

theorem coeff_list_prod_of_natDegree_le (l : List S[X]) (n : ℕ) (hl : ∀ p ∈ l, natDegree p ≤ n) :
    coeff (List.prod l) (l.length * n) = (l.map fun p => coeff p n).prod := by
  induction' l with hd tl IH
  · simp
  · have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
    simp only [List.prod_cons, List.map, List.length]
    rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]
    have h : natDegree tl.prod ≤ n * tl.length := by
      refine (natDegree_list_prod_le _).trans ?_
      rw [← tl.length_map natDegree, mul_comm]
      refine List.sum_le_card_nsmul _ _ ?_
      simpa using hl'
    exact coeff_mul_add_eq_of_natDegree_le (hl _ List.mem_cons_self) h

Coefficient of High-Degree Term in Product of Polynomials with Bounded Degree

Informal description

Let $l$ be a list of univariate polynomials over a semiring $S$, and let $n$ be a natural number such that for every polynomial $p \in l$, the natural degree of $p$ satisfies $\mathrm{natDegree}(p) \leq n$. Then the coefficient of $X^{k}$ in the product of all polynomials in $l$, where $k$ is the product of the length of $l$ and $n$, is equal to the product of the coefficients of $X^n$ in each polynomial $p \in l$. That is, \[ \text{coeff}\left(\prod_{p \in l} p, |l| \cdot n\right) = \prod_{p \in l} \text{coeff}(p, n). \]

Polynomial.natDegree_multiset_prod_le theorem

: t.prod.natDegree ≤ (t.map natDegree).sum

Full source

theorem natDegree_multiset_prod_le : t.prod.natDegree ≤ (t.map natDegree).sum :=
  Quotient.inductionOn t (by simpa using natDegree_list_prod_le)

Upper Bound on Natural Degree of Polynomial Product in a Multiset

Informal description

For any multiset $t$ of univariate polynomials over a semiring $S$, the natural degree of the product of polynomials in $t$ is less than or equal to the sum of the natural degrees of the polynomials in $t$. That is, $\mathrm{natDegree}(\prod_{p \in t} p) \leq \sum_{p \in t} \mathrm{natDegree}(p)$.

Polynomial.natDegree_prod_le theorem

: (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree

Full source

theorem natDegree_prod_le : (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree := by
  simpa using natDegree_multiset_prod_le (s.1.map f)

Upper Bound on Natural Degree of Finite Product of Polynomials: $\mathrm{natDegree}(\prod f_i) \leq \sum \mathrm{natDegree}(f_i)$

Informal description

For any finite set $s$ and any family of univariate polynomials $(f_i)_{i \in s}$ over a semiring, the natural degree of the product $\prod_{i \in s} f_i$ is less than or equal to the sum of the natural degrees of the polynomials $f_i$, i.e., \[ \mathrm{natDegree}\left(\prod_{i \in s} f_i\right) \leq \sum_{i \in s} \mathrm{natDegree}(f_i). \]

Polynomial.degree_multiset_prod_le theorem

: t.prod.degree ≤ (t.map Polynomial.degree).sum

Full source

/-- The degree of a product of polynomials is at most the sum of the degrees,
where the degree of the zero polynomial is ⊥.
-/
theorem degree_multiset_prod_le : t.prod.degree ≤ (t.map Polynomial.degree).sum :=
  Quotient.inductionOn t (by simpa using degree_list_prod_le)

Degree Bound for Product of Polynomials in a Multiset: $\deg(\prod t) \leq \sum (\deg \circ t)$

Informal description

For any multiset $t$ of univariate polynomials over a semiring, the degree of the product of the polynomials in $t$ is less than or equal to the sum of the degrees of the individual polynomials in $t$. Here, the degree of the zero polynomial is considered to be $\bot$.

Polynomial.degree_prod_le theorem

: (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

Full source

theorem degree_prod_le : (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree := by
  simpa only [Multiset.map_map] using degree_multiset_prod_le (s.1.map f)

Degree Bound for Finite Product of Polynomials: $\deg(\prod f_i) \leq \sum \deg(f_i)$

Informal description

For any finite set $s$ and any family of univariate polynomials $(f_i)_{i \in s}$ over a semiring $R$, the degree of the product $\prod_{i \in s} f_i$ is less than or equal to the sum of the degrees of the individual polynomials $f_i$. That is, \[ \deg\left(\prod_{i \in s} f_i\right) \leq \sum_{i \in s} \deg(f_i). \]

Polynomial.leadingCoeff_multiset_prod' theorem

(h : (t.map leadingCoeff).prod ≠ 0) : t.prod.leadingCoeff = (t.map leadingCoeff).prod

Full source

/-- 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 leadingCoeff_multiset_prod' (h : (t.map leadingCoeff).prod ≠ 0) :
    t.prod.leadingCoeff = (t.map leadingCoeff).prod := by
  induction' t using Multiset.induction_on with a t ih; · simp
  simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
  rw [Polynomial.leadingCoeff_mul']
  · rw [ih]
    simp only [ne_eq]
    apply right_ne_zero_of_mul h
  · rw [ih]
    · exact h
    simp only [ne_eq, not_false_eq_true]
    apply right_ne_zero_of_mul h

Leading Coefficient of Multiset Product of Polynomials

Informal description

Let $R$ be a commutative semiring and let $t$ be a multiset of polynomials in $R[X]$. If the product of the leading coefficients of the polynomials in $t$ is nonzero, then the leading coefficient of the product of the polynomials in $t$ is equal to the product of their leading coefficients. That is, $$ \text{leadingCoeff}\left(\prod_{p \in t} p\right) = \prod_{p \in t} \text{leadingCoeff}(p). $$

Polynomial.leadingCoeff_prod' theorem

(h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Full source

/-- 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 leadingCoeff_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) :
    (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff := by
  simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)

Leading Coefficient of Polynomial Product under Nonzero Condition

Informal description

Let $R$ be a commutative semiring and let $s$ be a finite set. For a family of polynomials $(f_i)_{i \in s}$ in $R[X]$, if the product of their leading coefficients $\prod_{i \in s} \text{leadingCoeff}(f_i)$ is nonzero, then the leading coefficient of the product polynomial $\prod_{i \in s} f_i$ is equal to the product of their leading coefficients: \[ \text{leadingCoeff}\left(\prod_{i \in s} f_i\right) = \prod_{i \in s} \text{leadingCoeff}(f_i). \]

Polynomial.natDegree_multiset_prod' theorem

(h : (t.map fun f => leadingCoeff f).prod ≠ 0) : t.prod.natDegree = (t.map fun f => natDegree f).sum

Full source

/-- 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 natDegree_multiset_prod' (h : (t.map fun f => leadingCoeff f).prod ≠ 0) :
    t.prod.natDegree = (t.map fun f => natDegree f).sum := by
  revert h
  refine Multiset.induction_on t ?_ fun a t ih ht => ?_; · simp
  rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢
  rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
  · apply right_ne_zero_of_mul ht
  · rwa [Polynomial.leadingCoeff_multiset_prod']
    apply right_ne_zero_of_mul ht

Natural Degree of Multiset Product of Polynomials with Nonzero Leading Coefficient Product

Informal description

Let $R$ be a commutative semiring and let $t$ be a multiset of polynomials in $R[X]$. If the product of the leading coefficients of the polynomials in $t$ is nonzero, then the natural degree of the product of the polynomials in $t$ equals the sum of their natural degrees. That is, $$ \text{natDegree}\left(\prod_{f \in t} f\right) = \sum_{f \in t} \text{natDegree}(f). $$

Polynomial.natDegree_prod' theorem

(h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Full source

/-- 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 natDegree_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree := by
  simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)

Degree of Polynomial Product Equals Sum of Degrees When Leading Coefficients Multiply to Nonzero

Informal description

Let $R$ be a commutative semiring, $s$ a finite set, and $(f_i)_{i \in s}$ a family of polynomials in $R[X]$. If the product of their leading coefficients $\prod_{i \in s} \text{lc}(f_i)$ is nonzero, then the natural degree of the product polynomial $\prod_{i \in s} f_i$ equals the sum of their natural degrees: \[ \deg\left(\prod_{i \in s} f_i\right) = \sum_{i \in s} \deg(f_i). \]

Polynomial.natDegree_multiset_prod_of_monic theorem

(h : ∀ f ∈ t, Monic f) : t.prod.natDegree = (t.map natDegree).sum

Full source

theorem natDegree_multiset_prod_of_monic (h : ∀ f ∈ t, Monic f) :
    t.prod.natDegree = (t.map natDegree).sum := by
  nontriviality R
  apply natDegree_multiset_prod'
  suffices (t.map fun f => leadingCoeff f).prod = 1 by
    rw [this]
    simp
  convert prod_replicate (Multiset.card t) (1 : R)
  · simp only [eq_replicate, Multiset.card_map, eq_self_iff_true, true_and]
    rintro i hi
    obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hi
    apply h
    assumption
  · simp

Natural Degree of Product of Monic Polynomials in Multiset Form

Informal description

Let $R$ be a commutative semiring and let $t$ be a multiset of monic polynomials in $R[X]$. Then the natural degree of the product of the polynomials in $t$ equals the sum of their natural degrees, i.e., $$ \text{natDegree}\left(\prod_{f \in t} f\right) = \sum_{f \in t} \text{natDegree}(f). $$

Polynomial.degree_multiset_prod_of_monic theorem

[Nontrivial R] (h : ∀ f ∈ t, Monic f) : t.prod.degree = (t.map degree).sum

Full source

theorem degree_multiset_prod_of_monic [Nontrivial R] (h : ∀ f ∈ t, Monic f) :
    t.prod.degree = (t.map degree).sum := by
  have : t.prod ≠ 0 := Monic.ne_zero <| by simpa using monic_multiset_prod_of_monic _ _ h
  rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
    Multiset.map_map, Function.comp_def,
    Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]

Degree of Product of Monic Polynomials in Multiset Form Equals Sum of Degrees

Informal description

Let $R$ be a nontrivial commutative semiring and let $t$ be a multiset of monic polynomials in $R[X]$. Then the degree of the product of the polynomials in $t$ equals the sum of their degrees, i.e., \[ \deg\left(\prod_{f \in t} f\right) = \sum_{f \in t} \deg(f). \]

Polynomial.natDegree_prod_of_monic theorem

(h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Full source

theorem natDegree_prod_of_monic (h : ∀ i ∈ s, (f i).Monic) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree := by
  simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Natural Degree of Product of Monic Polynomials over Finite Set

Informal description

Let $R$ be a commutative semiring, $s$ a finite set, and $f : s \to R[X]$ a family of monic polynomials. Then the natural degree of the product $\prod_{i \in s} f(i)$ equals the sum of the natural degrees of the $f(i)$, i.e., $$ \text{natDegree}\left(\prod_{i \in s} f(i)\right) = \sum_{i \in s} \text{natDegree}(f(i)). $$

Polynomial.degree_prod_of_monic theorem

[Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

Full source

theorem degree_prod_of_monic [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) :
    (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree := by
  simpa using degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Degree of Product of Monic Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a nontrivial commutative semiring, $s$ a finite set, and $f : s \to R[X]$ a family of monic polynomials. Then the degree of the product $\prod_{i \in s} f(i)$ equals the sum of the degrees of the $f(i)$, i.e., \[ \deg\left(\prod_{i \in s} f(i)\right) = \sum_{i \in s} \deg(f(i)). \]

Polynomial.coeff_multiset_prod_of_natDegree_le theorem

 (n : ℕ) (hl : ∀ p ∈ t, natDegree p ≤ n) : coeff t.prod ((Multiset.card t) * n) = (t.map fun p => coeff p n).prod

Full source

theorem coeff_multiset_prod_of_natDegree_le (n : ℕ) (hl : ∀ p ∈ t, natDegree p ≤ n) :
    coeff t.prod ((Multiset.card t) * n) = (t.map fun p => coeff p n).prod := by
  induction t using Quotient.inductionOn
  simpa using coeff_list_prod_of_natDegree_le _ _ hl

Coefficient of High-Degree Term in Product of Polynomials with Bounded Degree

Informal description

Let $R$ be a commutative semiring and $t$ a multiset of polynomials in $R[X]$. For a natural number $n$, suppose that every polynomial $p \in t$ satisfies $\mathrm{natDegree}(p) \leq n$. Then the coefficient of $X^{k}$ in the product of all polynomials in $t$, where $k$ is the product of the cardinality of $t$ and $n$, is equal to the product of the coefficients of $X^n$ in each polynomial $p \in t$. That is, \[ \text{coeff}\left(\prod_{p \in t} p, |t| \cdot n\right) = \prod_{p \in t} \text{coeff}(p, n). \]

Polynomial.coeff_prod_of_natDegree_le theorem

 (f : ι → R[X]) (n : ℕ) (h : ∀ p ∈ s, natDegree (f p) ≤ n) : coeff (∏ i ∈ s, f i) (#s * n) = ∏ i ∈ s, coeff (f i) n

Full source

theorem coeff_prod_of_natDegree_le (f : ι → R[X]) (n : ℕ) (h : ∀ p ∈ s, natDegree (f p) ≤ n) :
    coeff (∏ i ∈ s, f i) (#s * n) = ∏ i ∈ s, coeff (f i) n := by
  obtain ⟨l, hl⟩ := s
  convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
  · simp
  · simp
  · simpa using h

Coefficient of high-degree term in product of polynomials with bounded degree

Informal description

Let $R$ be a commutative semiring, $s$ a finite set, and $f : \iota \to R[X]$ a family of polynomials. For a natural number $n$, suppose that for every $p \in s$, the natural degree of $f(p)$ satisfies $\mathrm{natDegree}(f(p)) \leq n$. Then the coefficient of $X^{k}$ in the product $\prod_{i \in s} f(i)$, where $k = \#s \cdot n$, is equal to the product of the coefficients of $X^n$ in each polynomial $f(i)$. That is, \[ \text{coeff}\left(\prod_{i \in s} f(i), \#s \cdot n\right) = \prod_{i \in s} \text{coeff}(f(i), n). \]

Polynomial.coeff_zero_multiset_prod theorem

: t.prod.coeff 0 = (t.map fun f => coeff f 0).prod

Full source

theorem coeff_zero_multiset_prod : t.prod.coeff 0 = (t.map fun f => coeff f 0).prod := by
  refine Multiset.induction_on t ?_ fun a t ht => ?_; · simp
  rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]

Constant Term of Product Equals Product of Constant Terms for Polynomial Multisets

Informal description

For any multiset $t$ of polynomials over a commutative semiring $R$, the constant term (coefficient of $X^0$) of the product of all polynomials in $t$ is equal to the product of the constant terms of each polynomial in $t$. That is, $$ \text{coeff}\left(\prod_{f \in t} f, 0\right) = \prod_{f \in t} \text{coeff}(f, 0). $$

Polynomial.coeff_zero_prod theorem

: (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Full source

theorem coeff_zero_prod : (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0 := by
  simpa using coeff_zero_multiset_prod (s.1.map f)

Constant Term of Polynomial Product Equals Product of Constant Terms

Informal description

For any finite set $s$ and any family of polynomials $(f_i)_{i \in s}$ over a commutative semiring $R$, the constant term (coefficient of $X^0$) of the product $\prod_{i \in s} f_i$ is equal to the product of the constant terms of each $f_i$, i.e., $$ \left(\prod_{i \in s} f_i\right)\!\!(0) = \prod_{i \in s} f_i(0). $$

Polynomial.multiset_prod_X_sub_C_nextCoeff theorem

(t : Multiset R) : nextCoeff (t.map fun x => X - C x).prod = -t.sum

Full source

theorem multiset_prod_X_sub_C_nextCoeff (t : Multiset R) :
    nextCoeff (t.map fun x => X - C x).prod = -t.sum := by
  rw [nextCoeff_multiset_prod]
  · simp only [nextCoeff_X_sub_C]
    exact t.sum_hom (-AddMonoidHom.id R)
  · intros
    apply monic_X_sub_C

Next coefficient of product of linear factors equals negative sum: $\text{nextCoeff}(\prod_{x \in t} (X - x)) = -\sum_{x \in t} x$

Informal description

For any multiset $t$ of elements in a commutative ring $R$, the next coefficient (i.e., the coefficient of $X^{n-1}$ where $n$ is the cardinality of $t$) of the product $\prod_{x \in t} (X - x)$ is equal to the negative of the sum of all elements in $t$.

Polynomial.prod_X_sub_C_nextCoeff theorem

{s : Finset ι} (f : ι → R) : nextCoeff (∏ i ∈ s, (X - C (f i))) = -∑ i ∈ s, f i

Full source

theorem prod_X_sub_C_nextCoeff {s : Finset ι} (f : ι → R) :
    nextCoeff (∏ i ∈ s, (X - C (f i))) = -∑ i ∈ s, f i := by
  simpa using multiset_prod_X_sub_C_nextCoeff (s.1.map f)

Next coefficient of product of linear factors equals negative sum: $\text{nextCoeff}(\prod_{i \in s} (X - f(i))) = -\sum_{i \in s} f(i)$

Informal description

For any finite set $s$ and any function $f : \iota \to R$ where $R$ is a commutative ring, the next coefficient (i.e., the coefficient of $X^{n-1}$ where $n$ is the cardinality of $s$) of the product $\prod_{i \in s} (X - f(i))$ is equal to the negative of the sum $\sum_{i \in s} f(i)$.

Polynomial.multiset_prod_X_sub_C_coeff_card_pred theorem

(t : Multiset R) (ht : 0 < Multiset.card t) : (t.map fun x => X - C x).prod.coeff ((Multiset.card t) - 1) = -t.sum

Full source

theorem multiset_prod_X_sub_C_coeff_card_pred (t : Multiset R) (ht : 0 < Multiset.card t) :
    (t.map fun x => X - C x).prod.coeff ((Multiset.card t) - 1) = -t.sum := by
  nontriviality R
  convert multiset_prod_X_sub_C_nextCoeff (by assumption)
  rw [nextCoeff, if_neg]
  swap
  · rw [natDegree_multiset_prod_of_monic]
    swap
    · simp only [Multiset.mem_map]
      rintro _ ⟨_, _, rfl⟩
      apply monic_X_sub_C
    simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]
    obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
    exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩
  congr; rw [natDegree_multiset_prod_of_monic] <;> · simp [natDegree_X_sub_C, monic_X_sub_C]

Coefficient of $X^{n-1}$ in Product of Linear Factors Equals Negative Sum

Informal description

Let $R$ be a commutative ring and let $t$ be a non-empty multiset of elements in $R$. The coefficient of $X^{n-1}$ in the product $\prod_{x \in t} (X - x)$, where $n$ is the cardinality of $t$, equals the negative of the sum of all elements in $t$, i.e., \[ \text{coeff}\left(\prod_{x \in t} (X - x), n-1\right) = -\sum_{x \in t} x. \]

Polynomial.prod_X_sub_C_coeff_card_pred theorem

(s : Finset ι) (f : ι → R) (hs : 0 < #s) : (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Full source

theorem prod_X_sub_C_coeff_card_pred (s : Finset ι) (f : ι → R) (hs : 0 < #s) :
    (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i := by
  simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)

Coefficient of $X^{n-1}$ in Product of Linear Factors Equals Negative Sum

Informal description

Let $R$ be a commutative ring, $\iota$ a type, $s$ a non-empty finite subset of $\iota$, and $f : \iota \to R$ a function. The coefficient of $X^{n-1}$ in the product $\prod_{i \in s} (X - f(i))$, where $n$ is the cardinality of $s$, equals the negative of the sum of all $f(i)$ for $i \in s$, i.e., \[ \text{coeff}\left(\prod_{i \in s} (X - f(i)), n-1\right) = -\sum_{i \in s} f(i). \]

Polynomial.natDegree_multiset_prod_X_sub_C_eq_card theorem

(s : Multiset R) : (s.map (X - C ·)).prod.natDegree = Multiset.card s

Full source

@[simp]
lemma natDegree_multiset_prod_X_sub_C_eq_card (s : Multiset R) :
    (s.map (X - C ·)).prod.natDegree = Multiset.card s := by
  rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
  · simp only [(· ∘ ·), natDegree_X_sub_C, Multiset.map_const', Multiset.sum_replicate, smul_eq_mul,
      mul_one]
  · exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

Natural Degree of Product of Linear Polynomials Equals Multiset Cardinality

Informal description

Let $R$ be a commutative ring and let $s$ be a multiset of elements in $R$. The natural degree of the product of the linear polynomials $(X - a)$ for each $a \in s$ is equal to the cardinality of $s$, i.e., \[ \text{natDegree}\left(\prod_{a \in s} (X - a)\right) = \text{card}(s). \]

Polynomial.natDegree_finset_prod_X_sub_C_eq_card theorem

{α} (s : Finset α) (f : α → R) : (∏ a ∈ s, (X - C (f a))).natDegree = s.card

Full source

@[simp] lemma natDegree_finset_prod_X_sub_C_eq_card {α} (s : Finset α) (f : α → R) :
    (∏ a ∈ s, (X - C (f a))).natDegree = s.card := by
  rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]

Degree of Product of Linear Polynomials Equals Cardinality of Index Set

Informal description

Let $R$ be a commutative ring, $\alpha$ a type, $s$ a finite subset of $\alpha$, and $f : \alpha \to R$ a function. The natural degree of the product $\prod_{a \in s} (X - f(a))$ in the polynomial ring $R[X]$ is equal to the cardinality of $s$, i.e., \[ \deg\left(\prod_{a \in s} (X - f(a))\right) = \#s. \]

Polynomial.degree_list_prod theorem

[Nontrivial R] (l : List R[X]) : l.prod.degree = (l.map degree).sum

Full source

/-- 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 degree_list_prod [Nontrivial R] (l : List R[X]) : l.prod.degree = (l.map degree).sum :=
  map_list_prod (@degreeMonoidHom R _ _ _) l

Degree of Product of Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a nontrivial semiring and let $l$ be a list of polynomials over $R$. The degree of the product of the polynomials in $l$ is equal to the sum of the degrees of the polynomials in $l$, where the degree of the zero polynomial is considered to be $\bot$.

Polynomial.natDegree_prod theorem

(h : ∀ i ∈ s, f i ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Full source

/-- 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 natDegree_prod (h : ∀ i ∈ s, f i ≠ 0) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree := by
  nontriviality R
  apply natDegree_prod'
  rw [prod_ne_zero_iff]
  intro x hx; simp [h x hx]

Degree of Product of Nonzero Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a commutative semiring, $s$ a finite set, and $(f_i)_{i \in s}$ a family of nonzero polynomials in $R[X]$. Then the degree of the product polynomial $\prod_{i \in s} f_i$ equals the sum of the degrees of the $f_i$: \[ \deg\left(\prod_{i \in s} f_i\right) = \sum_{i \in s} \deg(f_i). \]

Polynomial.natDegree_multiset_prod theorem

(h : (0 : R[X]) ∉ t) : natDegree t.prod = (t.map natDegree).sum

Full source

theorem natDegree_multiset_prod (h : (0 : R[X]) ∉ t) :
    natDegree t.prod = (t.map natDegree).sum := by
  nontriviality R
  rw [natDegree_multiset_prod']
  simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]
  rintro ⟨_, h, rfl⟩
  contradiction

Natural Degree of Product of Nonzero Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a commutative semiring and let $t$ be a multiset of polynomials in $R[X]$. If none of the polynomials in $t$ is the zero polynomial, then the natural degree of the product of the polynomials in $t$ equals the sum of their natural degrees, i.e., \[ \text{natDegree}\left(\prod_{f \in t} f\right) = \sum_{f \in t} \text{natDegree}(f). \]

Polynomial.degree_multiset_prod theorem

[Nontrivial R] : t.prod.degree = (t.map fun f => degree f).sum

Full source

/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
-/
theorem degree_multiset_prod [Nontrivial R] : t.prod.degree = (t.map fun f => degree f).sum :=
  map_multiset_prod (@degreeMonoidHom R _ _ _) _

Degree of Product of Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a nontrivial commutative semiring and $t$ be a multiset of polynomials over $R$. Then the degree of the product of polynomials in $t$ is equal to the sum of the degrees of the individual polynomials in $t$, i.e., \[ \deg\left(\prod_{f \in t} f\right) = \sum_{f \in t} \deg(f). \]

Polynomial.degree_prod theorem

[Nontrivial R] : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

Full source

/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
-/
theorem degree_prod [Nontrivial R] : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree :=
  map_prod (@degreeMonoidHom R _ _ _) _ _

Degree of Product of Polynomials Equals Sum of Degrees

Informal description

Let $R$ be a nontrivial semiring and let $f : \alpha \to R[X]$ be a function. For any finite set $s \subseteq \alpha$, the degree of the product $\prod_{i \in s} f(i)$ is equal to the sum of the degrees of the polynomials $f(i)$ for $i \in s$.

Polynomial.leadingCoeff_multiset_prod theorem

: t.prod.leadingCoeff = (t.map fun f => leadingCoeff f).prod

Full source

/-- 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 leadingCoeff_multiset_prod :
    t.prod.leadingCoeff = (t.map fun f => leadingCoeff f).prod := by
  rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
  simp only [leadingCoeffHom_apply]

Leading Coefficient of a Multiset Product of Polynomials

Informal description

For a multiset $t$ of polynomials over a commutative semiring $R$, the leading coefficient of the product of all polynomials in $t$ is equal to the product of the leading coefficients of each polynomial in $t$. That is, \[ \text{leadingCoeff}\left(\prod_{f \in t} f\right) = \prod_{f \in t} \text{leadingCoeff}(f). \]

Polynomial.leadingCoeff_prod theorem

: (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Full source

/-- 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.
-/
theorem leadingCoeff_prod : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff := by
  simpa using leadingCoeff_multiset_prod (s.1.map f)

Leading Coefficient of Product of Polynomials Equals Product of Leading Coefficients

Informal description

Let $R$ be a commutative semiring and let $f : \alpha \to R[X]$ be a function. For any finite set $s \subseteq \alpha$, the leading coefficient of the product $\prod_{i \in s} f(i)$ is equal to the product of the leading coefficients of the polynomials $f(i)$ for $i \in s$. That is, \[ \text{leadingCoeff}\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} \text{leadingCoeff}(f(i)). \]

Main results