Documentation

Mathlib.Algebra.MvPolynomial.Degrees

Degrees of polynomials #

This file establishes many results about the degree of a multivariate polynomial.

The degree set of a polynomial $P \in R[X]$ is a Multiset containing, for each $x$ in the variable set, $n$ copies of $x$, where $n$ is the maximum number of copies of $x$ appearing in a monomial of $P$.

Main declarations #

Notation #

As in other polynomial files, we typically use the notation:

degrees #

def MvPolynomial.degrees {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.

(For example, degrees (x^2 * y + y^3) would be {x, x, y, y, y}.)

Equations
  • p.degrees = p.support.sup fun (s : σ →₀ ) => Finsupp.toMultiset s
Instances For
    theorem MvPolynomial.degrees_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) :
    p.degrees = p.support.sup fun (s : σ →₀ ) => Finsupp.toMultiset s
    theorem MvPolynomial.degrees_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) (a : R) :
    ((MvPolynomial.monomial s) a).degrees Finsupp.toMultiset s
    theorem MvPolynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) (a : R) (ha : a 0) :
    ((MvPolynomial.monomial s) a).degrees = Finsupp.toMultiset s
    theorem MvPolynomial.degrees_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :
    (MvPolynomial.C a).degrees = 0
    theorem MvPolynomial.degrees_X' {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :
    (MvPolynomial.X n).degrees {n}
    @[simp]
    theorem MvPolynomial.degrees_X {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (n : σ) :
    (MvPolynomial.X n).degrees = {n}
    @[simp]
    @[simp]
    theorem MvPolynomial.degrees_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
    (p + q).degrees p.degrees q.degrees
    theorem MvPolynomial.degrees_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] (s : Finset ι) (f : ιMvPolynomial σ R) :
    (∑ is, f i).degrees s.sup fun (i : ι) => (f i).degrees
    theorem MvPolynomial.degrees_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
    (p * q).degrees p.degrees + q.degrees
    theorem MvPolynomial.degrees_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ιMvPolynomial σ R) :
    (∏ is, f i).degrees is, (f i).degrees
    theorem MvPolynomial.degrees_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (n : ) :
    (p ^ n).degrees n p.degrees
    theorem MvPolynomial.mem_degrees {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} :
    i p.degrees ∃ (d : σ →₀ ), MvPolynomial.coeff d p 0 i d.support
    theorem MvPolynomial.le_degrees_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : p.degrees.Disjoint q.degrees) :
    p.degrees (p + q).degrees
    theorem MvPolynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : p.degrees.Disjoint q.degrees) :
    (p + q).degrees = p.degrees q.degrees
    theorem MvPolynomial.degrees_map {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) :
    ((MvPolynomial.map f) p).degrees p.degrees
    theorem MvPolynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : στ) (φ : MvPolynomial σ R) :
    ((MvPolynomial.rename f) φ).degrees Multiset.map f φ.degrees
    theorem MvPolynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S} (hf : Function.Injective f) :
    ((MvPolynomial.map f) p).degrees = p.degrees
    theorem MvPolynomial.degrees_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {f : στ} (h : Function.Injective f) :
    ((MvPolynomial.rename f) p).degrees = Multiset.map f p.degrees

    degreeOf #

    def MvPolynomial.degreeOf {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (p : MvPolynomial σ R) :

    degreeOf n p gives the highest power of X_n that appears in p

    Equations
    Instances For
      theorem MvPolynomial.degreeOf_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (n : σ) (p : MvPolynomial σ R) :
      theorem MvPolynomial.degreeOf_eq_sup {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f : MvPolynomial σ R) :
      MvPolynomial.degreeOf n f = f.support.sup fun (m : σ →₀ ) => m n
      theorem MvPolynomial.degreeOf_lt_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : } (h : 0 < d) :
      MvPolynomial.degreeOf n f < d mf.support, m n < d
      theorem MvPolynomial.degreeOf_le_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : } :
      MvPolynomial.degreeOf n f d mf.support, m n d
      @[simp]
      theorem MvPolynomial.degreeOf_zero {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :
      @[simp]
      theorem MvPolynomial.degreeOf_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) (x : σ) :
      MvPolynomial.degreeOf x (MvPolynomial.C a) = 0
      theorem MvPolynomial.degreeOf_X {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (j : σ) [Nontrivial R] :
      MvPolynomial.degreeOf i (MvPolynomial.X j) = if i = j then 1 else 0
      theorem MvPolynomial.monomial_le_degreeOf {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) {f : MvPolynomial σ R} {m : σ →₀ } (h_m : m f.support) :
      theorem MvPolynomial.degreeOf_mul_X_ne {R : Type u} {σ : Type u_1} [CommSemiring R] {i : σ} {j : σ} (f : MvPolynomial σ R) (h : i j) :
      theorem MvPolynomial.degreeOf_C_mul_le {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R) :
      theorem MvPolynomial.degreeOf_mul_C_le {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R) :
      theorem MvPolynomial.degreeOf_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {f : στ} (h : Function.Injective f) (i : σ) :

      totalDegree #

      def MvPolynomial.totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

      totalDegree p gives the maximum |s| over the monomials X^s in p

      Equations
      • p.totalDegree = p.support.sup fun (s : σ →₀ ) => s.sum fun (x : σ) (e : ) => e
      Instances For
        theorem MvPolynomial.totalDegree_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
        p.totalDegree = p.support.sup fun (m : σ →₀ ) => Multiset.card (Finsupp.toMultiset m)
        theorem MvPolynomial.le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ } (h : s p.support) :
        (s.sum fun (x : σ) (e : ) => e) p.totalDegree
        theorem MvPolynomial.totalDegree_le_degrees_card {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
        p.totalDegree Multiset.card p.degrees
        theorem MvPolynomial.totalDegree_le_of_support_subset {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : p.support q.support) :
        p.totalDegree q.totalDegree
        @[simp]
        theorem MvPolynomial.totalDegree_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :
        (MvPolynomial.C a).totalDegree = 0
        @[simp]
        theorem MvPolynomial.totalDegree_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] [Nontrivial R] (s : σ) :
        (MvPolynomial.X s).totalDegree = 1
        theorem MvPolynomial.totalDegree_add {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (b : MvPolynomial σ R) :
        (a + b).totalDegree max a.totalDegree b.totalDegree
        theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
        (p + q).totalDegree = p.totalDegree
        theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
        (q + p).totalDegree = p.totalDegree
        theorem MvPolynomial.totalDegree_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (b : MvPolynomial σ R) :
        (a * b).totalDegree a.totalDegree + b.totalDegree
        theorem MvPolynomial.totalDegree_smul_le {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :
        (a f).totalDegree f.totalDegree
        theorem MvPolynomial.totalDegree_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (n : ) :
        (a ^ n).totalDegree n * a.totalDegree
        @[simp]
        theorem MvPolynomial.totalDegree_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) {c : R} (hc : c 0) :
        ((MvPolynomial.monomial s) c).totalDegree = s.sum fun (x : σ) (e : ) => e
        theorem MvPolynomial.totalDegree_monomial_le {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) (c : R) :
        ((MvPolynomial.monomial s) c).totalDegree s.sum fun (x : σ) => id
        @[simp]
        theorem MvPolynomial.totalDegree_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ) :
        (MvPolynomial.X s ^ n).totalDegree = n
        theorem MvPolynomial.totalDegree_list_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (s : List (MvPolynomial σ R)) :
        s.prod.totalDegree (List.map MvPolynomial.totalDegree s).sum
        theorem MvPolynomial.totalDegree_multiset_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Multiset (MvPolynomial σ R)) :
        s.prod.totalDegree (Multiset.map MvPolynomial.totalDegree s).sum
        theorem MvPolynomial.totalDegree_finset_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ιMvPolynomial σ R) :
        (s.prod f).totalDegree is, (f i).totalDegree
        theorem MvPolynomial.totalDegree_finset_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ιMvPolynomial σ R) :
        (s.sum f).totalDegree s.sup fun (i : ι) => (f i).totalDegree
        theorem MvPolynomial.totalDegree_finsetSum_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ιMvPolynomial σ R} {d : } (hf : is, (f i).totalDegree d) :
        (s.sum f).totalDegree d
        theorem MvPolynomial.degreeOf_le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] (f : MvPolynomial σ R) (i : σ) :
        MvPolynomial.degreeOf i f f.totalDegree
        theorem MvPolynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] [Fintype σ] (f : MvPolynomial σ R) (n : ) (h : f.totalDegree < n * Fintype.card σ) {d : σ →₀ } (hd : d f.support) :
        ∃ (i : σ), d i < n
        theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ } (h : f.totalDegree < id.support, d i) :
        theorem MvPolynomial.totalDegree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : στ) (p : MvPolynomial σ R) :
        ((MvPolynomial.rename f) p).totalDegree p.totalDegree