Degree and support of univariate polynomials

Main results

• Polynomial.as_sum_support: write p : R[X] as a sum over its support
• Polynomial.as_sum_range: write p : R[X] as a sum over {0, ..., natDegree p}
• Polynomial.natDegree_mem_support_of_nonzero: natDegree p ∈ support p if p ≠ 0

theorem Polynomial.supDegree_eq_natDegree {R : Type u} [Semiring R] (p : Polynomial R) : AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

theorem Polynomial.le_natDegree_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → a ≤ p.natDegree

theorem Polynomial.supp_subset_range {R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (h : p.natDegree < m) : p.support ⊆ Finset.range m

theorem Polynomial.supp_subset_range_natDegree_succ {R : Type u} [Semiring R] {p : Polynomial R} : p.support ⊆ Finset.range (p.natDegree + 1)

theorem Polynomial.as_sum_support {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i

theorem Polynomial.sum_over_range' {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) (n : ℕ) (w : p.natDegree < n) : p.sum f = ∑ a ∈ Finset.range n, f a (p.coeff a)

We can reexpress a sum over p.support as a sum over range n, for any n satisfying p.natDegree < n.

theorem Polynomial.sum_over_range {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) : p.sum f = ∑ a ∈ Finset.range (p.natDegree + 1), f a (p.coeff a)

We can reexpress a sum over p.support as a sum over range (p.natDegree + 1).

theorem Polynomial.sum_fin {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {n : ℕ} {p : Polynomial R} (hn : p.degree < ↑n) : ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

theorem Polynomial.as_sum_range' {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (w : p.natDegree < n) : p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_range {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_range_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i

theorem Polynomial.mem_support_C_mul_X_pow {R : Type u} [Semiring R] {n a : ℕ} {c : R} (h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support) : a = n

theorem Polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [Semiring R] {c : R} {n : ℕ} : (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1

theorem Polynomial.card_supp_le_succ_natDegree {R : Type u} [Semiring R] (p : Polynomial R) : p.support.card ≤ p.natDegree + 1

theorem Polynomial.le_degree_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → ↑a ≤ p.degree

theorem Polynomial.nonempty_support_iff {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ p ≠ 0

theorem Polynomial.natDegree_mem_support_of_nonzero {R : Type u} [Semiring R] {p : Polynomial R} (H : p ≠ 0) : p.natDegree ∈ p.support

theorem Polynomial.natDegree_eq_support_max' {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.natDegree = p.support.max' ⋯