Degree and leading coefficient of polynomials with respect to a monomial order

We consider a type σ of indeterminates and a commutative semiring R and a monomial order m : MonomialOrder σ.

• m.degree f is the degree of f for the monomial ordering m

• m.leadingCoeff f is the leading coefficient of f for the monomial ordering m

• m.leadingCoeff_ne_zero_iff f asserts that this coefficient is nonzero iff f ≠ 0.

• in a field, m.isUnit_leadingCoeff f asserts that this coefficient is a unit iff f ≠ 0.

• m.degree_add_le : the m.degree of f + g is smaller than or equal to the supremum of those of f and g

• m.degree_add_of_lt h : the m.degree of f + g is equal to that of f if the m.degree of g is strictly smaller than that f

• m.leadingCoeff_add_of_lt h: then, the leading coefficient of f + g is that of f .

• m.degree_add_of_ne h : the m.degree of f + g is equal to that the supremum of those of f and g if they are distinct

• m.degree_sub_le : the m.degree of f - g is smaller than or equal to the supremum of those of f and g

• m.degree_sub_of_lt h : the m.degree of f - g is equal to that of f if the m.degree of g is strictly smaller than that f

• m.leadingCoeff_sub_of_lt h: then, the leading coefficient of f - g is that of f .

• m.degree_mul_le: the m.degree of f * g is smaller than or equal to the sum of those of f and g.

• m.degree_mul_of_isRegular_left, m.degree_mul_of_isRegular_right and m.degree_mul assert the equality when the leading coefficient of f or g is regular, or when R is a domain and f and g are nonzero.

• m.leadingCoeff_mul_of_isRegular_left, m.leadingCoeff_mul_of_isRegular_right and m.leadingCoeff_mul say that m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Reference

[Becker-Weispfenning1993]

def MonomialOrder.degree {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) : σ →₀ ℕ

the degree of a multivariate polynomial with respect to a monomial ordering

Equations

• m.degree f = m.toSyn.symm (f.support.sup ⇑m.toSyn)

def MonomialOrder.leadingCoeff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) : R

the leading coefficient of a multivariate polynomial with respect to a monomial ordering

Equations

• m.leadingCoeff f = MvPolynomial.coeff (m.degree f) f

@[deprecated MonomialOrder.leadingCoeff (since := "2025-01-31")]

def MonomialOrder.lCoeff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) : R

Alias of MonomialOrder.leadingCoeff.

---

the leading coefficient of a multivariate polynomial with respect to a monomial ordering

Equations

• @MonomialOrder.lCoeff = @MonomialOrder.leadingCoeff

@[simp]

theorem MonomialOrder.degree_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : m.degree 0 = 0

@[simp]

theorem MonomialOrder.leadingCoeff_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : m.leadingCoeff 0 = 0

@[deprecated MonomialOrder.leadingCoeff_zero (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : m.leadingCoeff 0 = 0

Alias of MonomialOrder.leadingCoeff_zero.

theorem MonomialOrder.degree_monomial_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} (c : R) : m.toSyn (m.degree ((MvPolynomial.monomial d) c)) ≤ m.toSyn d

theorem MonomialOrder.degree_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} (c : R) [Decidable (c = 0)] : m.degree ((MvPolynomial.monomial d) c) = if c = 0 then 0 else d

theorem MonomialOrder.degree_X_le_single {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} : m.toSyn (m.degree (MvPolynomial.X s)) ≤ m.toSyn (Finsupp.single s 1)

theorem MonomialOrder.degree_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Nontrivial R] {s : σ} : m.degree (MvPolynomial.X s) = Finsupp.single s 1

@[simp]

theorem MonomialOrder.leadingCoeff_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} (c : R) : m.leadingCoeff ((MvPolynomial.monomial d) c) = c

@[deprecated MonomialOrder.leadingCoeff_monomial (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} (c : R) : m.leadingCoeff ((MvPolynomial.monomial d) c) = c

Alias of MonomialOrder.leadingCoeff_monomial.

theorem MonomialOrder.degree_le_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} : m.toSyn (m.degree f) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d

theorem MonomialOrder.degree_lt_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : m.toSyn 0 < m.toSyn d) : m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

theorem MonomialOrder.le_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ f.support) : m.toSyn d ≤ m.toSyn (m.degree f)

theorem MonomialOrder.coeff_eq_zero_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : m.toSyn (m.degree f) < m.toSyn d) : MvPolynomial.coeff d f = 0

theorem MonomialOrder.leadingCoeff_ne_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : m.leadingCoeff f ≠ 0 ↔ f ≠ 0

@[deprecated MonomialOrder.leadingCoeff_ne_zero_iff (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_ne_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : m.leadingCoeff f ≠ 0 ↔ f ≠ 0

Alias of MonomialOrder.leadingCoeff_ne_zero_iff.

@[simp]

theorem MonomialOrder.leadingCoeff_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : m.leadingCoeff f = 0 ↔ f = 0

@[deprecated MonomialOrder.leadingCoeff_eq_zero_iff (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : m.leadingCoeff f = 0 ↔ f = 0

Alias of MonomialOrder.leadingCoeff_eq_zero_iff.

theorem MonomialOrder.coeff_degree_ne_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : MvPolynomial.coeff (m.degree f) f ≠ 0 ↔ f ≠ 0

@[simp]

theorem MonomialOrder.coeff_degree_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : MvPolynomial.coeff (m.degree f) f = 0 ↔ f = 0

theorem MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : m.degree f = 0 ↔ f.totalDegree = 0

@[simp]

theorem MonomialOrder.degree_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (r : R) : m.degree (MvPolynomial.C r) = 0

theorem MonomialOrder.eq_C_of_degree_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.degree f = 0) : f = MvPolynomial.C (m.leadingCoeff f)

theorem MonomialOrder.degree_add_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} : m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

theorem MonomialOrder.degree_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.degree (f + g) = m.degree f

theorem MonomialOrder.leadingCoeff_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.leadingCoeff (f + g) = m.leadingCoeff f

@[deprecated MonomialOrder.leadingCoeff_add_of_lt (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.leadingCoeff (f + g) = m.leadingCoeff f

Alias of MonomialOrder.leadingCoeff_add_of_lt.

theorem MonomialOrder.degree_add_of_ne {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.degree f ≠ m.degree g) : m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

theorem MonomialOrder.degree_mul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} : m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f + m.degree g)

theorem MonomialOrder.coeff_mul_of_add_of_degree_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} {a b : σ →₀ ℕ} (ha : m.toSyn (m.degree f) ≤ m.toSyn a) (hb : m.toSyn (m.degree g) ≤ m.toSyn b) : MvPolynomial.coeff (a + b) (f * g) = MvPolynomial.coeff a f * MvPolynomial.coeff b g

Multiplicativity of leading coefficients

theorem MonomialOrder.coeff_mul_of_degree_add {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} : MvPolynomial.coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) : m.degree (f * g) = m.degree f + m.degree g

Multiplicativity of leading coefficients

theorem MonomialOrder.leadingCoeff_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

@[deprecated MonomialOrder.leadingCoeff_mul_of_isRegular_left (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_left.

---

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) : m.degree (f * g) = m.degree f + m.degree g

Multiplicativity of leading coefficients

theorem MonomialOrder.leadingCoeff_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

@[deprecated MonomialOrder.leadingCoeff_mul_of_isRegular_right (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_right.

---

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) : m.degree (f * g) = m.degree f + m.degree g

Degree of product

theorem MonomialOrder.degree_mul_of_nonzero_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hfg : f * g ≠ 0) : m.degree (f * g) = m.degree f + m.degree g

Degree of of product

theorem MonomialOrder.leadingCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

@[deprecated MonomialOrder.leadingCoeff_mul (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Alias of MonomialOrder.leadingCoeff_mul.

---

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_smul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} {f : MvPolynomial σ R} : m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)

theorem MonomialOrder.degree_smul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} (hr : IsRegular r) {f : MvPolynomial σ R} : m.degree (r • f) = m.degree f

theorem MonomialOrder.degree_prod_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R} {s : Finset ι} : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))

theorem MonomialOrder.coeff_prod_sum_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (P : ι → MvPolynomial σ R) (s : Finset ι) : MvPolynomial.coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

theorem MonomialOrder.degree_prod_of_regular {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) : m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

theorem MonomialOrder.degree_prod {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {ι : Type u_3} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, P i ≠ 0) : m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

theorem MonomialOrder.leadingCoeff_prod_of_regular {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) : m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

@[simp]

theorem MonomialOrder.degree_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} : m.degree (-f) = m.degree f

theorem MonomialOrder.degree_sub_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} : m.toSyn (m.degree (f - g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

theorem MonomialOrder.degree_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.degree (f - g) = m.degree f

theorem MonomialOrder.leadingCoeff_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.leadingCoeff (f - g) = m.leadingCoeff f

@[deprecated MonomialOrder.leadingCoeff_sub_of_lt (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) : m.leadingCoeff (f - g) = m.leadingCoeff f

Alias of MonomialOrder.leadingCoeff_sub_of_lt.

theorem MonomialOrder.isUnit_leadingCoeff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {f : MvPolynomial σ R} : IsUnit (m.leadingCoeff f) ↔ f ≠ 0

@[deprecated MonomialOrder.isUnit_leadingCoeff (since := "2025-01-31")]

theorem MonomialOrder.lCoeff_is_unit_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {f : MvPolynomial σ R} : IsUnit (m.leadingCoeff f) ↔ f ≠ 0

Alias of MonomialOrder.isUnit_leadingCoeff.