Main degree of a polynomial

This file defines the main degree of a multivariate polynomial, which is the degree with respect to its main variable.

Main definitions

• MvPolynomial.mainDegree p: The degree of p with respect to its main variable. If max_vars p = ⊥ (i.e., p is a constant or zero), the degree is 0.

Main theorems

• mainDegree_eq_zero_iff: p.mainDegree = 0 iff p.max_vars = ⊥
• mainDegree_of_max_vars_isSome: When p.max_vars = c ≠ ⊥, p.mainDegree = p.degreeOf c

noncomputable def MvPolynomial.mainDegree {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) : ℕ

The "main degree" of p: the degree of p with respect to its main variable. If max_vars p = ⊥ (i.e., p is a constant or zero), the degree is 0.

Equations

• p.mainDegree = match p.vars.max with | none => 0 | some c => MvPolynomial.degreeOf c p

theorem MvPolynomial.mainDegree_of_max_vars_isSome {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} : p.vars.max = ↑c → p.mainDegree = degreeOf c p

theorem MvPolynomial.mainDegree_of_max_vars_isSome' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} : p.vars.max = ↑c → p.mainDegree = p.support.sup fun (s : σ →₀ ℕ) => s c

theorem MvPolynomial.mainDegree_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] : p.mainDegree = 0 ↔ p.vars.max = ⊥

theorem MvPolynomial.mainDegree_eq_zero_iff_eq_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] : p.mainDegree = 0 ↔ p = C (coeff 0 p)

theorem MvPolynomial.degreeOf_max_vars_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} : p.vars.max = ↑c → degreeOf c p ≠ 0

theorem MvPolynomial.max_vars_mem_degrees {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} : p.vars.max = ↑c → c ∈ p.degrees

@[simp]

theorem MvPolynomial.mainDegree_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : mainDegree 0 = 0

@[simp]

theorem MvPolynomial.mainDegree_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {c : σ} {s : σ →₀ ℕ} {r : R} (hr : r ≠ 0) (hs : s.support.max = ↑c) : ((monomial s) r).mainDegree = s c

@[simp]

theorem MvPolynomial.mainDegree_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (r : R) : (C r).mainDegree = 0

@[simp]

theorem MvPolynomial.mainDegree_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] (i : σ) (k : ℕ) : (X i ^ k).mainDegree = k

@[simp]

theorem MvPolynomial.mainDegree_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] (i : σ) : (X i).mainDegree = 1