Groebner.MonomialOrder

@[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.monic_one' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

m.Monic 1

source

@[simp]

theorem MonomialOrder.monic_of_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton (MvPolynomial σ 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.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

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

source

theorem MonomialOrder.sPolynomial_decomposition_of_degree_sum_smul_le₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_4} [CommRing R] {d : m.syn} {ι : Type u_3} {B : Finset ι} {c : ι → R} {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, c b • g b)) < d) :

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

source

theorem MonomialOrder.sPolynomial_decomposition_of_degree_sum_smul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_4} [CommRing R] {d : m.syn} {ι : Type u_3} {B : Finset ι} {c : ι → R} {g : ι → MvPolynomial σ R} (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff (g b))) (hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d) (hfd : m.toSyn (m.degree (∑ b ∈ B, c b • g b)) < d) :

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

source

theorem MonomialOrder.sPolynomial_decomposition_of_degree_sum_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_4} [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.sPolynomial_monomial_mul_of_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {p₁ p₂ : MvPolynomial σ R} (hp₁ : m.leadingCoeff p₁ ∈ nonZeroDivisors R) (hp₂ : m.leadingCoeff p₂ ∈ nonZeroDivisors 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_of_mem_nonZeroDivisors' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {p₁ p₂ : MvPolynomial σ R} (hp₁ : m.leadingCoeff p₁ ∈ nonZeroDivisors R) (hp₂ : m.leadingCoeff p₂ ∈ nonZeroDivisors 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.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.support_add_of_leadingTerm_add_leadingTerm_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} (h : m.leadingTerm p + m.leadingTerm q = 0) (a : σ →₀ ℕ) :

a ∈ (p + q).support → a ∈ p.support ∧ m.toSyn a < m.toSyn (m.degree p) ∨ a ∈ q.support ∧ m.toSyn a < m.toSyn (m.degree q)

source

@[simp]

theorem MonomialOrder.leadingTerm_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] (p : MvPolynomial σ R) :

m.leadingTerm (-p) = -m.leadingTerm p

source

theorem MonomialOrder.support_sub_of_leadingTerm_eq_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {p q : MvPolynomial σ R} (h : m.leadingTerm p = m.leadingTerm q) (a : σ →₀ ℕ) :

a ∈ (p - q).support → a ∈ p.support ∧ m.toSyn a < m.toSyn (m.degree p) ∨ a ∈ q.support ∧ m.toSyn a < m.toSyn (m.degree q)

source

theorem MonomialOrder.degree_rename_killCompl_le_degree {σ : Type u_1} {m : MonomialOrder σ} {σ' : Type u_2} {R : Type u_3} [CommSemiring R] {f : σ' → σ} (hf : Function.Injective f) {p : MvPolynomial σ R} :

m.toSyn (m.degree ((MvPolynomial.rename f) ((MvPolynomial.killCompl hf) p))) ≤ m.toSyn (m.degree p)

source

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

WithBot (σ →₀ ℕ)

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

Equations

m.withBotDegree f = WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max

Instances For

source

noncomputable def MonomialOrder.toWithBotSyn {σ : Type u_1} (m : MonomialOrder σ) :

WithBot (σ →₀ ℕ) ≃+ WithBot m.syn

Equations

m.toWithBotSyn = m.toSyn.withBotCongr

Instances For

source

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_bot {σ : Type u_1} {m : MonomialOrder σ} :

m.toWithBotSyn ⊥ = ⊥

source

@[simp]

theorem MonomialOrder.toWithBotSyn_symm_apply_bot {σ : Type u_1} {m : MonomialOrder σ} :

m.toWithBotSyn.symm ⊥ = ⊥

source

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_eq_bot_iff {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) :

m.toWithBotSyn a = ⊥ ↔ a = ⊥

source

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_le_bot_iff {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) :

m.toWithBotSyn a ≤ ⊥ ↔ a = ⊥

source

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_coe {σ : Type u_1} {m : MonomialOrder σ} (a : σ →₀ ℕ) :

m.toWithBotSyn ↑a = ↑(m.toSyn a)

source

@[simp]

theorem MonomialOrder.bot_lt_toWithBotSyn_apply_iff {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) :

⊥ < m.toWithBotSyn a ↔ a ≠ ⊥

source

@[simp]

theorem MonomialOrder.toWithBotSyn_symm_apply_eq_bot {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot m.syn) :

m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥

source

theorem MonomialOrder.toWithBotSyn_apply {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) :

m.toWithBotSyn a = WithBot.map (⇑m.toSyn) a

source

def MonomialOrder.«term_≺'[_]_» :

Lean.TrailingParserDescr

Given a monomial order with bot, notation for the corresponding strict order relation on WithBot (σ →₀ ℕ)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def MonomialOrder.«term_≼'[_]_» :

Lean.TrailingParserDescr

Given a monomial order with bot, notation for the corresponding order relation on WithBot (σ →₀ ℕ)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

m.withBotDegree f = if f = 0 then ⊥ else ↑(m.degree f)

source

@[simp]

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

m.withBotDegree f = ↑(m.degree f) ↔ f ≠ 0

source

@[simp]

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

m.withBotDegree f = ⊥ ↔ f = 0

source

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

m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

source

@[simp]

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

m.withBotDegree 0 = ⊥

source

theorem MonomialOrder.withBotDegree_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (c : R) [Decidable (c = 0)] :

m.withBotDegree ((MvPolynomial.monomial d) c) = if c = 0 then ⊥ else ↑d

source

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

m.withBotDegree (MvPolynomial.C c) = if c = 0 then ⊥ else 0

source

@[simp]

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

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

source

@[simp]

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

m.withBotDegree (-f) = m.withBotDegree f

source

@[simp]

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

m.withBotDegree 1 = 0

source

theorem MonomialOrder.withBotDegree_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.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

source

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

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

source

@[simp]

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

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

source

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

m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f + m.withBotDegree g)

source

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

m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)

source

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

m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

source

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

m.withBotDegree f ≤ m.withBotDegree g ↔ m.degree f ≤ m.degree g ∧ (g = 0 → f = 0)

source

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

m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

source

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

m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

source

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

m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) < m.toSyn (m.degree g)

source

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

m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

source

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

m.toWithBotSyn (m.withBotDegree (f + g)) ≤ max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

source

theorem MonomialOrder.withBotDegree_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) (h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)) :

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

source

theorem MonomialOrder.withBotDegree_add_of_right_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) (h : m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g)) :

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

source

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

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

source

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

m.toWithBotSyn ↑d ≤ m.toWithBotSyn (m.withBotDegree f)

source

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

m.toWithBotSyn (m.withBotDegree p) ≤ m.toWithBotSyn (m.withBotDegree q)

source

theorem MonomialOrder.withBotDegree_rename_killCompl_le_withBotDegree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {σ' : Type u_3} {f : σ' → σ} (hf : Function.Injective f) (p : MvPolynomial σ R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename f) ((MvPolynomial.killCompl hf) p))) ≤ m.toWithBotSyn (m.withBotDegree p)