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.Monic f asserts that the leading coefficient of f is 1.

• 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_mul_leadingCoeff_ne_zero : if the product of the leading coefficients is non zero, then the degree is the sum of the degrees.

• m.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero : if the product of the leading coefficients is non zero, then the leading coefficient is that product.

• 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

• m.degree_pow_of_pow_leadingCoeff_ne_zero : is the nth power of the leading coefficient of f is non zero, then the degree of f ^ n is n • (m.degree f)

• m.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero : is the nth power of the leading coefficient of f is non zero, then the leading coefficient of f ^ n is that power.

• m.degree_prod_of_regular : the degree of a product of polynomials whose leading coefficients are regular is the sum of their degrees.

• m.leadingCoeff_prod_of_regular : the leading coefficient of a product of polynomials whose leading coefficients are regular is the product of their leading coefficients.

• m.Monic.prod : a product of monic polynomials is monic.

Reference

[BW93]

def MonomialOrder.degree {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : Finsupp σ Nat

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

Equations

• Eq (m.degree f) (DFunLike.coe m.toSyn.symm (f.support.sup (DFunLike.coe m.toSyn)))

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

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

Equations

• Eq (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_2} [CommSemiring R] (f : MvPolynomial σ R) : R

Alias of MonomialOrder.leadingCoeff.

---

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

Equations

• Eq @MonomialOrder.lCoeff @MonomialOrder.leadingCoeff

def MonomialOrder.Monic {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : Prop

A multivariate polynomial is Monic with respect to a monomial order if its leading coefficient (for that monomial order) is 1.

Equations

• Eq (m.Monic f) (Eq (m.leadingCoeff f) 1)

theorem MonomialOrder.Monic.of_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton R] {f : MvPolynomial σ R} : m.Monic f

def MonomialOrder.Monic.decidable {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [DecidableEq R] (f : MvPolynomial σ R) : Decidable (m.Monic f)

Equations

• Eq (MonomialOrder.Monic.decidable f) (id inferInstance)

theorem MonomialOrder.Monic.leadingCoeff_eq_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.Monic f) : Eq (m.leadingCoeff f) 1

theorem MonomialOrder.Monic.coeff_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.Monic f) : Eq (MvPolynomial.coeff (m.degree f) f) 1

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

theorem MonomialOrder.degree_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton R] {f : MvPolynomial σ R} : Eq (m.degree f) 0

theorem MonomialOrder.leadingCoeff_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : Eq (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] : Eq (m.leadingCoeff 0) 0

Alias of MonomialOrder.leadingCoeff_zero.

theorem MonomialOrder.Monic.ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Nontrivial R] {f : MvPolynomial σ R} (hf : m.Monic f) : Ne f 0

theorem MonomialOrder.degree_monomial_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : Finsupp σ Nat} (c : R) : LE.le (DFunLike.coe m.toSyn (m.degree (DFunLike.coe (MvPolynomial.monomial d) c))) (DFunLike.coe m.toSyn d)

theorem MonomialOrder.degree_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : Finsupp σ Nat} (c : R) [Decidable (Eq c 0)] : Eq (m.degree (DFunLike.coe (MvPolynomial.monomial d) c)) (ite (Eq c 0) 0 d)

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

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

theorem MonomialOrder.degree_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : Eq (m.degree 1) 0

theorem MonomialOrder.leadingCoeff_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : Finsupp σ Nat} (c : R) : Eq (m.leadingCoeff (DFunLike.coe (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 : Finsupp σ Nat} (c : R) : Eq (m.leadingCoeff (DFunLike.coe (MvPolynomial.monomial d) c)) c

Alias of MonomialOrder.leadingCoeff_monomial.

theorem MonomialOrder.monic_monomial_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : Finsupp σ Nat} : m.Monic (DFunLike.coe (MvPolynomial.monomial d) 1)

theorem MonomialOrder.monic_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : Finsupp σ Nat} {c : R} : Iff (m.Monic (DFunLike.coe (MvPolynomial.monomial d) c)) (Eq c 1)

theorem MonomialOrder.leadingCoeff_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} : Eq (m.leadingCoeff (MvPolynomial.X s)) 1

theorem MonomialOrder.monic_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} : m.Monic (MvPolynomial.X s)

theorem MonomialOrder.leadingCoeff_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : Eq (m.leadingCoeff 1) 1

theorem MonomialOrder.monic_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : m.Monic (DFunLike.coe MvPolynomial.C 1)

theorem MonomialOrder.degree_le_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : Finsupp σ Nat} : Iff (LE.le (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe m.toSyn d)) (∀ (c : Finsupp σ Nat), Membership.mem f.support c → LE.le (DFunLike.coe m.toSyn c) (DFunLike.coe m.toSyn d))

theorem MonomialOrder.degree_lt_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : Finsupp σ Nat} (hd : LT.lt (DFunLike.coe m.toSyn 0) (DFunLike.coe m.toSyn d)) : Iff (LT.lt (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe m.toSyn d)) (∀ (c : Finsupp σ Nat), Membership.mem f.support c → LT.lt (DFunLike.coe m.toSyn c) (DFunLike.coe m.toSyn d))

theorem MonomialOrder.le_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : Finsupp σ Nat} (hd : Membership.mem f.support d) : LE.le (DFunLike.coe m.toSyn d) (DFunLike.coe 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 : Finsupp σ Nat} (hd : LT.lt (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe m.toSyn d)) : Eq (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} : Iff (Ne (m.leadingCoeff f) 0) (Ne 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} : Iff (Ne (m.leadingCoeff f) 0) (Ne f 0)

Alias of MonomialOrder.leadingCoeff_ne_zero_iff.

theorem MonomialOrder.leadingCoeff_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : Iff (Eq (m.leadingCoeff f) 0) (Eq 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} : Iff (Eq (m.leadingCoeff f) 0) (Eq 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} : Iff (Ne (MvPolynomial.coeff (m.degree f) f) 0) (Ne f 0)

theorem MonomialOrder.coeff_degree_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} : Iff (Eq (MvPolynomial.coeff (m.degree f) f) 0) (Eq 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} : Iff (Eq (m.degree f) 0) (Eq f.totalDegree 0)

theorem MonomialOrder.degree_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (r : R) : Eq (m.degree (DFunLike.coe 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 : Eq (m.degree f) 0) : Eq f (DFunLike.coe 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} : LE.le (DFunLike.coe m.toSyn (m.degree (HAdd.hAdd f g))) (Max.max (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.degree (HAdd.hAdd 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.leadingCoeff (HAdd.hAdd 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.leadingCoeff (HAdd.hAdd f g)) (m.leadingCoeff f)

Alias of MonomialOrder.leadingCoeff_add_of_lt.

theorem MonomialOrder.Monic.add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.Monic f) (h : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : m.Monic (HAdd.hAdd f g)

theorem MonomialOrder.degree_add_of_ne {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : Ne (m.degree f) (m.degree g)) : Eq (DFunLike.coe m.toSyn (m.degree (HAdd.hAdd f g))) (Max.max (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe 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} : LE.le (DFunLike.coe m.toSyn (m.degree (HMul.hMul f g))) (DFunLike.coe m.toSyn (HAdd.hAdd (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 : Finsupp σ Nat} (ha : LE.le (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe m.toSyn a)) (hb : LE.le (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn b)) : Eq (MvPolynomial.coeff (HAdd.hAdd a b) (HMul.hMul f g)) (HMul.hMul (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} : Eq (MvPolynomial.coeff (HAdd.hAdd (m.degree f) (m.degree g)) (HMul.hMul f g)) (HMul.hMul (m.leadingCoeff f) (m.leadingCoeff g))

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hfg : Ne (HMul.hMul (m.leadingCoeff f) (m.leadingCoeff g)) 0) : Eq (m.degree (HMul.hMul f g)) (HAdd.hAdd (m.degree f) (m.degree g))

Monomial degree of product

theorem MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hfg : Ne (HMul.hMul (m.leadingCoeff f) (m.leadingCoeff g)) 0) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (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 : Ne g 0) : Eq (m.degree (HMul.hMul f g)) (HAdd.hAdd (m.degree f) (m.degree g))

Monomial degree of product

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 : Ne g 0) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (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 : Ne g 0) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (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 : Ne f 0) (hg : IsRegular (m.leadingCoeff g)) : Eq (m.degree (HMul.hMul f g)) (HAdd.hAdd (m.degree f) (m.degree g))

Monomial degree of product

theorem MonomialOrder.leadingCoeff_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : Ne f 0) (hg : IsRegular (m.leadingCoeff g)) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (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 : Ne f 0) (hg : IsRegular (m.leadingCoeff g)) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (m.leadingCoeff f) (m.leadingCoeff g))

Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_right.

---

Multiplicativity of leading coefficients

theorem MonomialOrder.Monic.mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.Monic f) (hg : m.Monic g) : m.Monic (HMul.hMul f g)

theorem MonomialOrder.degree_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : Ne f 0) (hg : Ne g 0) : Eq (m.degree (HMul.hMul f g)) (HAdd.hAdd (m.degree f) (m.degree g))

Monomial degree of product

theorem MonomialOrder.leadingCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : Ne f 0) (hg : Ne g 0) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (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 : Ne f 0) (hg : Ne g 0) : Eq (m.leadingCoeff (HMul.hMul f g)) (HMul.hMul (m.leadingCoeff f) (m.leadingCoeff g))

Alias of MonomialOrder.leadingCoeff_mul.

---

Multiplicativity of leading coefficients

theorem MonomialOrder.degree_pow_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (n : Nat) : LE.le (DFunLike.coe m.toSyn (m.degree (HPow.hPow f n))) (DFunLike.coe m.toSyn (HSMul.hSMul n (m.degree f)))

Monomial degree of powers

theorem MonomialOrder.coeff_pow_nsmul_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (n : Nat) : Eq (MvPolynomial.coeff (HSMul.hSMul n (m.degree f)) (HPow.hPow f n)) (HPow.hPow (m.leadingCoeff f) n)

theorem MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {n : Nat} (hf : Ne (HPow.hPow (m.leadingCoeff f) n) 0) : Eq (m.degree (HPow.hPow f n)) (HSMul.hSMul n (m.degree f))

Monomial degree of powers

theorem MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {n : Nat} (hf : Ne (HPow.hPow (m.leadingCoeff f) n) 0) : Eq (m.leadingCoeff (HPow.hPow f n)) (HPow.hPow (m.leadingCoeff f) n)

Leading coefficient of powers

theorem MonomialOrder.Monic.pow {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {n : Nat} (hf : m.Monic f) : m.Monic (HPow.hPow f n)

theorem MonomialOrder.degree_pow {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsReduced R] (f : MvPolynomial σ R) (n : Nat) : Eq (m.degree (HPow.hPow f n)) (HSMul.hSMul n (m.degree f))

Monomial degree of powers (in a reduced ring)

theorem MonomialOrder.leadingCoeff_pow {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsReduced R] (f : MvPolynomial σ R) (n : Nat) : Eq (m.leadingCoeff (HPow.hPow f n)) (HPow.hPow (m.leadingCoeff f) n)

Leading coefficient of powers (in a reduced ring)

theorem MonomialOrder.degree_smul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} {f : MvPolynomial σ R} : LE.le (DFunLike.coe m.toSyn (m.degree (HSMul.hSMul r f))) (DFunLike.coe 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} : Eq (m.degree (HSMul.hSMul 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 ι} : LE.le (DFunLike.coe m.toSyn (m.degree (s.prod fun (i : ι) => P i))) (DFunLike.coe m.toSyn (s.sum fun (i : ι) => 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 ι) : Eq (MvPolynomial.coeff (s.sum fun (i : ι) => m.degree (P i)) (s.prod fun (i : ι) => P i)) (s.prod fun (i : ι) => 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 : ι), Membership.mem s i → IsRegular (m.leadingCoeff (P i))) : Eq (m.degree (s.prod fun (i : ι) => P i)) (s.sum fun (i : ι) => 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 : ι), Membership.mem s i → Ne (P i) 0) : Eq (m.degree (s.prod fun (i : ι) => P i)) (s.sum fun (i : ι) => 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 : ι), Membership.mem s i → IsRegular (m.leadingCoeff (P i))) : Eq (m.leadingCoeff (s.prod fun (i : ι) => P i)) (s.prod fun (i : ι) => m.leadingCoeff (P i))

theorem MonomialOrder.Monic.prod {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ (i : ι), Membership.mem s i → m.Monic (P i)) : m.Monic (s.prod fun (i : ι) => P i)

A product of monic polynomials is monic

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

theorem MonomialOrder.leadingCoeff_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} : Eq (m.leadingCoeff (Neg.neg f)) (Neg.neg (m.leadingCoeff f))

theorem MonomialOrder.degree_sub_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} : LE.le (DFunLike.coe m.toSyn (m.degree (HSub.hSub f g))) (Max.max (DFunLike.coe m.toSyn (m.degree f)) (DFunLike.coe 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.degree (HSub.hSub 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.leadingCoeff (HSub.hSub 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 : LT.lt (DFunLike.coe m.toSyn (m.degree g)) (DFunLike.coe m.toSyn (m.degree f))) : Eq (m.leadingCoeff (HSub.hSub 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} : Iff (IsUnit (m.leadingCoeff f)) (Ne 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} : Iff (IsUnit (m.leadingCoeff f)) (Ne f 0)

Alias of MonomialOrder.isUnit_leadingCoeff.

theorem MonomialOrder.degree_X_add_C {R : Type u_2} [CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) : Eq (m.degree (HAdd.hAdd (MvPolynomial.X i) (DFunLike.coe MvPolynomial.C r))) (Finsupp.single i 1)

theorem MonomialOrder.degree_X_sub_C {R : Type u_2} [CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) : Eq (m.degree (HSub.hSub (MvPolynomial.X i) (DFunLike.coe MvPolynomial.C r))) (Finsupp.single i 1)

theorem MonomialOrder.monic_X_add_C {R : Type u_2} [CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) : m.Monic (HAdd.hAdd (MvPolynomial.X i) (DFunLike.coe MvPolynomial.C r))

theorem MonomialOrder.monic_X_sub_C {R : Type u_2} [CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) : m.Monic (HSub.hSub (MvPolynomial.X i) (DFunLike.coe MvPolynomial.C r))