Degree, leading coefficient and leading term 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.leadingTerm f is the leading term of f for the monomial ordering m.
m.sPolynomial f g is S-polynomial of f and g.
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 nonzero, 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 nonzero, then the leading coefficient is that product.
m.degree_mul_of_left_mem_nonZeroDivisors, m.degree_mul_of_right_mem_nonZeroDivisors and m.degree_mul assert the equality when the leading coefficient of f or g isn't zero divisors, or when R is a domain and f and g are nonzero.
m.leadingCoeff_mul_of_left_mem_nonZeroDivisors, m.leadingCoeff_mul_of_right_mem_nonZeroDivisors 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 nonzero, 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 nonzero, then the leading coefficient of f ^ n is that power.
m.degree_prod_of_mem_nonZeroDivisors : the degree of a product of polynomials whose leading coefficients aren't zero divisors is the sum of their degrees.
m.leadingCoeff_prod_of_mem_nonZeroDivisors : the leading coefficient of a product of polynomials whose leading coefficients aren't zero divisors is the product of their leading coefficients.
m.Monic.prod : a product of monic polynomials is monic.
m.degree_sub_leadingTerm_lt_iff : the degree of f - m.leadingTerm f is smaller than the degree of f if and only if m.degree f ≠ 0.

Reference #

[Becker-Weispfenning1993]

noncomputable def MonomialOrder.degree {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [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)

Instances For

source

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

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

Equations

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

Instances For

source

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

m.Monic f = (m.leadingCoeff f = 1)

Instances For

source

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

MvPolynomial σ R

The leading term of a multivariate polynomial with respect to a monomial ordering.

Equations

m.leadingTerm f = (MvPolynomial.monomial (m.degree f)) (m.leadingCoeff f)

Instances For

source

@[simp]

theorem MonomialOrder.C_mul_leadingCoeff_monomial_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) :

MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1 = m.leadingTerm p

source

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

m.Monic f

source

@[instance_reducible]

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

Decidable (m.Monic f)

Equations

MonomialOrder.Monic.decidable f = MonomialOrder.Monic.decidable._aux_1 f

source

@[simp]

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

m.leadingCoeff f = 1

source

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

MvPolynomial.coeff (m.degree f) f = 1

source

@[simp]

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

m.degree 0 = 0

source

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

f ≠ 0

source

@[simp]

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

m.degree f = 0

source

@[simp]

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

m.leadingCoeff 0 = 0

source

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) :

f ≠ 0

source

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

source

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

source

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)

source

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

source

@[simp]

theorem MonomialOrder.degree_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.degree 1 = 0

source

@[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

source

@[simp]

theorem MonomialOrder.monic_monomial_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} :

m.Monic ((MvPolynomial.monomial d) 1)

source

theorem MonomialOrder.monic_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} {c : R} :

m.Monic ((MvPolynomial.monomial d) c) ↔ c = 1

source

theorem MonomialOrder.leadingCoeff_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} :

m.leadingCoeff (MvPolynomial.X s) = 1

source

@[simp]

theorem MonomialOrder.monic_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} :

m.Monic (MvPolynomial.X s)

source

theorem MonomialOrder.leadingCoeff_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.leadingCoeff 1 = 1

source

theorem MonomialOrder.monic_C_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.Monic (MvPolynomial.C 1)

source

@[simp]

theorem MonomialOrder.monic_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.Monic 1

source

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

source

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

source

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)

source

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

source

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

source

@[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

source

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

source

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

m.degree f ∈ f.support ↔ f ≠ 0

source

@[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

source

theorem MonomialOrder.degree_mem_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (hp : p ≠ 0) :

m.degree p ∈ p.support

source

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

source

@[simp]

theorem MonomialOrder.degree_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (r : R) :

m.degree (MvPolynomial.C r) = 0

source

@[simp]

theorem MonomialOrder.leadingCoeff_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (c : R) :

m.leadingCoeff (MvPolynomial.C c) = c

source

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)

source

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

m.degree f = 0 ↔ f = MvPolynomial.C (m.leadingCoeff f)

source

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)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

source

theorem MonomialOrder.degree_sum_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {α : Type u_3} {s : Finset α} {f : α → MvPolynomial σ R} :

m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun (x : α) => m.toSyn (m.degree (f x))

source

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

source

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

m.degree (f + g) = m.degree g

source

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

source

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 : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :

m.Monic (f + g)

source

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)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

source

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)

source

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

source

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

source

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 : m.leadingCoeff f * m.leadingCoeff g ≠ 0) :

m.degree (f * g) = m.degree f + m.degree g

Monomial degree of product

source

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 : m.leadingCoeff f * m.leadingCoeff g ≠ 0) :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

source

theorem MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.leadingCoeff f ∈ nonZeroDivisors R) (hg : g ≠ 0) :

m.degree (f * g) = m.degree f + m.degree g

source

theorem MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : m.leadingCoeff g ∈ nonZeroDivisors R) :

m.degree (f * g) = m.degree f + m.degree g

source

theorem MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.leadingCoeff f ∈ nonZeroDivisors R) :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

source

theorem MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hg : m.leadingCoeff g ∈ nonZeroDivisors R) :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

source

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

Monomial degree of product

source

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)) :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

source

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

Monomial degree of product

source

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

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

source

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 (f * g)

source

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

m.degree (f * g) = m.degree f + m.degree g

Monomial degree of product

source

@[simp]

theorem MonomialOrder.leadingCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R} :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Multiplicativity of leading coefficients

source

theorem MonomialOrder.degree_pow_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (n : ℕ) :

m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)

Monomial degree of powers

source

theorem MonomialOrder.coeff_pow_nsmul_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (n : ℕ) :

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

source

theorem MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {n : ℕ} (hf : m.leadingCoeff f ^ n ≠ 0) :

m.degree (f ^ n) = n • m.degree f

Monomial degree of powers

source

theorem MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {n : ℕ} (hf : m.leadingCoeff f ^ n ≠ 0) :

m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Leading coefficient of powers

source

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

m.Monic (f ^ n)

source

theorem MonomialOrder.degree_pow {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsReduced R] (f : MvPolynomial σ R) (n : ℕ) :

m.degree (f ^ n) = n • m.degree f

Monomial degree of powers (in a reduced ring)

source

theorem MonomialOrder.leadingCoeff_pow {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsReduced R] (f : MvPolynomial σ R) (n : ℕ) :

m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Leading coefficient of powers (in a reduced ring)

source

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)

source

theorem MonomialOrder.degree_smul_of_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} (hr : r ∈ nonZeroDivisors R) {f : MvPolynomial σ R} :

m.degree (r • f) = m.degree f

source

theorem MonomialOrder.degree_smul_of_isRegular {σ : 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

source

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))

source

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)

source

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

m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

source

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)

source

theorem MonomialOrder.degree_prod {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors 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)

source

theorem MonomialOrder.degree_mul' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R} (hf : f * g ≠ 0) :

m.degree (f * g) = m.degree f + m.degree g

source

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

m.degree g ∉ f.support

source

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

m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

source

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)

source

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 ∈ s, m.Monic (P i)) :

m.Monic (∏ i ∈ s, P i)

A product of monic polynomials is monic

source

@[simp]

theorem MonomialOrder.leadingTerm_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) :

m.leadingTerm p = 0 ↔ p = 0

The leading term in a multivariate polynomial is zero if and only if this polynomial is zero.

source

@[simp]

theorem MonomialOrder.leadingTerm_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.leadingTerm 0 = 0

The leading term of the zero polynomial is zero

source

theorem MonomialOrder.image_leadingTerm_sdiff_singleton_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (B : Set (MvPolynomial σ R)) :

m.leadingTerm '' (B \ {0}) = m.leadingTerm '' B \ {0}

The set of leading terms of non-zero polynomials within a set B is equal to the set of leading terms of all polynomials within B, excluding zero.

source

theorem MonomialOrder.image_leadingTerm_insert_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (B : Set (MvPolynomial σ R)) :

m.leadingTerm '' insert 0 B = insert 0 (m.leadingTerm '' B)

The set of leading terms of zero and polynomials within a set B is equal to the set of zero and leading terms of polynomials within B.

source

@[simp]

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

m.degree (m.leadingTerm f) = m.degree f

The degree of f equals to the degree of leadingTerm f

source

@[simp]

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

m.leadingCoeff (m.leadingTerm f) = m.leadingCoeff f

source

@[simp]

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

m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

source

@[simp]

theorem MonomialOrder.leadingTerm_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (c : R) :

m.leadingTerm (MvPolynomial.C c) = MvPolynomial.C c

source

@[simp]

theorem MonomialOrder.leadingTerm_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) (c : R) :

m.leadingTerm ((MvPolynomial.monomial s) c) = (MvPolynomial.monomial s) c

source

@[simp]

theorem MonomialOrder.degree_leadingTerm_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] (p q : MvPolynomial σ R) :

m.degree (m.leadingTerm p * q) = m.degree (p * q)

source

@[simp]

theorem MonomialOrder.degree_mul_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] (p q : MvPolynomial σ R) :

m.degree (p * m.leadingTerm q) = m.degree (p * q)

source

theorem MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] {p p' q : MvPolynomial σ R} (hp : p ≠ 0) (h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))) :

m.toSyn (m.degree p) < m.toSyn (m.degree p')

source

theorem MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] {p p' q : MvPolynomial σ R} (hp : p ≠ 0) (hq : q ≠ 0) :

m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q)) ↔ m.toSyn (m.degree p) < m.toSyn (m.degree p')

source

@[simp]

theorem MonomialOrder.monic_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) :

m.Monic (m.leadingTerm p) ↔ m.Monic p

source

theorem MonomialOrder.support_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) [Decidable (p = 0)] :

(m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}

source

theorem MonomialOrder.support_leadingTerm' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (hp : p ≠ 0) :

(m.leadingTerm p).support = {m.degree p}

source

theorem MonomialOrder.le_degree_of_mem_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {a : σ →₀ ℕ} (ha : a ∈ p.support) :

m.toSyn a ≤ m.toSyn (m.degree p)

source

theorem MonomialOrder.leadingTerm_eq_leadingTerm_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} :

m.leadingTerm p = m.leadingTerm q ↔ m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

source

@[simp]

theorem MonomialOrder.leadingTerm_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] (p q : MvPolynomial σ R) :

m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q

source

@[simp]

theorem MonomialOrder.monic_of_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton R] (p : MvPolynomial σ R) :

m.Monic p

source

theorem MonomialOrder.degree_le_degree_of_support_subset {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} (h : p.support ⊆ q.support) :

m.toSyn (m.degree p) ≤ m.toSyn (m.degree q)

source

theorem MonomialOrder.toSyn_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.toSyn (m.degree g)

source

theorem MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.leadingCoeff f ∈ nonZeroDivisors R) :

f ∈ nonZeroDivisors (MvPolynomial σ R)

source

noncomputable def MonomialOrder.sPolynomial {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

MvPolynomial σ R

The S-polynomial of two polynomials.

Denoting

the leading monomial of polynomial $f$ and $g$ as $lm(f)$ and $lm(g)$,
the leading coefficient of $f$ and $g$ as $lc(f)$ and $lc(g)$ (formalized as m.leadingCoeff f and m.leadingCoeff g), and
the least common multiple of $lm(f)$ and $lm(g)$ as $lcm(lm(f),lm(g))$,

the S-polynomial of $f$ and $g$ is defined as $$sPoly(f,g) := (lcm(lm(f),lm(g)) / lm(f)) * lc(g) * f - (lcm(lm(f),lm(g)) / lm(g)) * lc(f) * g.$$

$(lcm(lm(f),lm(g)) / lm(f))$ and $lcm(lm(f),lm(g)) / lm(g)$ is formalized as monomial (m.degree g - m.degree f) 1 and monomial (m.degree g - m.degree f) 1, while there is also another more direct formalization in sPolynomial_def.

Notice that, when the polynomial ring is over a field, S-polynomial is usually defined as $$sPoly'(f,g) := (lcm(lm(f),lm(g)) / (lm(f) * lc(f))) * f - (lcm(lm(f),lm(g)) / (lm(g) * lc(g))) * g,$$ while we avoid inverting $lc(f)$ and $lc(g)$ in this formalization so that it doesn't require a field or units (IsUnit) over ring.

An equality between these two versions holds: $$sPoly(f,g) = lc(f) * lc(g) * sPoly'(f,g).$$

Equations

m.sPolynomial f g = (MvPolynomial.monomial (m.degree g - m.degree f)) (m.leadingCoeff g) * f - (MvPolynomial.monomial (m.degree f - m.degree g)) (m.leadingCoeff f) * g

Instances For

source

theorem MonomialOrder.sPolynomial_def {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

m.sPolynomial f g = (MvPolynomial.monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f - (MvPolynomial.monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g

source

theorem MonomialOrder.degree_ne_zero_of_sub_leadingTerm_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} (h : f - m.leadingTerm f ≠ 0) :

m.degree f ≠ 0

source

@[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

source

@[simp]

theorem MonomialOrder.leadingCoeff_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} :

m.leadingCoeff (-f) = -m.leadingCoeff f

source

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)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

source

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

source

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

source

theorem MonomialOrder.degree_sub_leadingTerm_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f : MvPolynomial σ R) :

m.toSyn (m.degree (f - m.leadingTerm f)) ≤ m.toSyn (m.degree f)

source

theorem MonomialOrder.degree_sub_leadingTerm_lt_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} (h : m.degree f ≠ 0) :

m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

source

theorem MonomialOrder.degree_sub_leadingTerm_lt_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} :

m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f) ↔ m.degree f ≠ 0

source

theorem MonomialOrder.sPolynomial_antisymm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

m.sPolynomial f g = -m.sPolynomial g f

source

@[simp]

theorem MonomialOrder.sPolynomial_left_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (g : MvPolynomial σ R) :

m.sPolynomial 0 g = 0

source

@[simp]

theorem MonomialOrder.sPolynomial_right_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f : MvPolynomial σ R) :

m.sPolynomial f 0 = 0

source

@[simp]

theorem MonomialOrder.sPolynomial_self {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f : MvPolynomial σ R) :

m.sPolynomial f f = 0

source

theorem MonomialOrder.degree_sPolynomial_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

source

theorem MonomialOrder.coeff_sPolynomial_sup_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

MvPolynomial.coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0

source

theorem MonomialOrder.degree_sPolynomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

source

theorem MonomialOrder.degree_sPolynomial_lt_sup_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.sPolynomial f g ≠ 0) :

m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g)

source

theorem MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.degree f = m.degree g) (hs : m.sPolynomial f g ≠ 0) :

m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f)

source

theorem MonomialOrder.sPolynomial_monomial_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] [NoZeroDivisors R] (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R) :

m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) = (MvPolynomial.monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) * m.sPolynomial p₁ p₂

source

theorem MonomialOrder.sPolynomial_monomial_mul' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] [NoZeroDivisors R] (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R) :

m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) = (MvPolynomial.monomial (m.degree ((MvPolynomial.monomial d₁) c₁ * p₁) ⊔ m.degree ((MvPolynomial.monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) * m.sPolynomial p₁ p₂

source

theorem MonomialOrder.sPolynomial_leadingTerm_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] [NoZeroDivisors R] (p₁ p₂ q₁ q₂ : MvPolynomial σ R) :

m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) = (MvPolynomial.monomial ((m.degree p₁ + m.degree q₁) ⊔ (m.degree p₂ + m.degree q₂) - m.degree q₁ ⊔ m.degree q₂)) (m.leadingCoeff p₁ * m.leadingCoeff p₂) * m.sPolynomial q₁ q₂

source

theorem MonomialOrder.sPolynomial_leadingTerm_mul' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] [NoZeroDivisors R] (p₁ p₂ q₁ q₂ : MvPolynomial σ R) :

m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) = (MvPolynomial.monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂)) (m.leadingCoeff p₁ * m.leadingCoeff p₂) * m.sPolynomial q₁ q₂

source

theorem MonomialOrder.sPolynomial_decomposition {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {d : m.syn} {ι : Type u_3} {B : Finset ι} {g : ι → MvPolynomial σ R} (hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) (hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d) :

∃ (c : ι → ι → R), ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

source

theorem MonomialOrder.isUnit_leadingCoeff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {f : MvPolynomial σ R} :

IsUnit (m.leadingCoeff f) ↔ f ≠ 0

source

theorem MonomialOrder.sPolynomial_decomposition' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {d : m.syn} {ι : Type u_3} {B : Finset ι} (g : ι → MvPolynomial σ R) (hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0) (hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d) :

∃ (c : ι → ι → R), ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

source

theorem MonomialOrder.degree_X_add_C {R : Type u_2} [CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) :

m.degree (MvPolynomial.X i + MvPolynomial.C r) = Finsupp.single i 1

source

theorem MonomialOrder.degree_X_sub_C {R : Type u_2} [CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) :

m.degree (MvPolynomial.X i - MvPolynomial.C r) = Finsupp.single i 1

source

theorem MonomialOrder.monic_X_add_C {R : Type u_2} [CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) :

m.Monic (MvPolynomial.X i + MvPolynomial.C r)

source

theorem MonomialOrder.monic_X_sub_C {R : Type u_2} [CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R) :

m.Monic (MvPolynomial.X i - MvPolynomial.C r)

Documentation

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Reference #