Documentation

CharacteristicSet.Basic

Characteristic Set Basics #

This file defines the fundamental concepts required for the Characteristic Set Method (Wu's Method), including the Class, Degree, Rank, and Reduction of multivariate polynomials.

Main Definitions #

MvPolynomial.mainVariable: The "main variable" of a polynomial, defined as the maximum variable index in its support.
MvPolynomial.mainDegree: The degree of the polynomial with respect to its main variable.
MvPolynomial.rank: A lexicographic combination of main variable and degree, defining a well-ordering on polynomials.
MvPolynomial.reducedTo: The predicate indicating that a polynomial q is reduced with respect to p (meaning q has lower degree in p's main variable).
MvPolynomial.reducedToSet: q is reduced with respect to every polynomial in a set.

Implementation Notes #

We assume a linear order on the variable type σ. The main variable mainVariable p is of type WithBot σ to handle the zero polynomial conveniently (where mainVariable 0 = ⊥).

def MvPolynomial.«term_[_]» :

Lean.TrailingParserDescr

Equations

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

Instances For

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

The main variable of a multivariate polynomial p is the largest variable index appearing in p. If p = 0, its main variable is ⊥.

Equations

p.mainVariable = p.support.sup fun (s : σ →₀ ℕ) => s.support.max

Instances For

theorem MvPolynomial.mainVariable_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) :

p.mainVariable = p.support.sup fun (s : σ →₀ ℕ) => s.support.max

@[simp]

theorem MvPolynomial.mainVariable_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

mainVariable 0 = ⊥

theorem MvPolynomial.ne_zero_of_mainVariable_ne_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] :

p.mainVariable ≠ ⊥ → p ≠ 0

@[simp]

theorem MvPolynomial.mainVariable_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {r : R} (s : σ →₀ ℕ) (hr : r ≠ 0) :

((monomial s) r).mainVariable = s.support.max

@[simp]

theorem MvPolynomial.mainVariable_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (r : R) :

(C r).mainVariable = ⊥

@[simp]

theorem MvPolynomial.mainVariable_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] (i : σ) {k : ℕ} (hk : k ≠ 0) :

(X i ^ k).mainVariable = ↑i

@[simp]

theorem MvPolynomial.mainVariable_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] (i : σ) :

(X i).mainVariable = ↑i

theorem MvPolynomial.mainVariable_eq_bot_iff_eq_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] :

p.mainVariable = ⊥ ↔ ∃ (r : R), p = C r

theorem MvPolynomial.mainVariable_add_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p q : MvPolynomial σ R) :

(p + q).mainVariable ≤ max p.mainVariable q.mainVariable

theorem MvPolynomial.mainVariable_mul_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p q : MvPolynomial σ R) :

(p * q).mainVariable ≤ max p.mainVariable q.mainVariable

theorem MvPolynomial.mainVariable_sum_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {α : Type u_3} (s : Finset α) (f : α → MvPolynomial σ R) :

(∑ a ∈ s, f a).mainVariable ≤ s.sup fun (a : α) => (f a).mainVariable

theorem MvPolynomial.mainVariable_prod_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {α : Type u_3} (s : Finset α) (f : α → MvPolynomial σ R) :

(∏ a ∈ s, f a).mainVariable ≤ s.sup fun (a : α) => (f a).mainVariable

theorem MvPolynomial.degreeOf_eq_zero_of_mainVariable_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {i : σ} :

p.mainVariable < ↑i → degreeOf i p = 0

theorem MvPolynomial.degreeOf_of_mainVariable_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] (i : σ) :

p.mainVariable = ⊥ → degreeOf i p = 0

theorem MvPolynomial.ne_zero_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} :

degreeOf i p ≠ 0 → p ≠ 0

theorem MvPolynomial.le_degreeOf_of_mem_support {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ} :

s ∈ p.support → s i ≤ degreeOf i p

theorem MvPolynomial.notMem_support_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ} :

degreeOf i p < s i → s ∉ p.support

@[simp]

theorem MvPolynomial.degreeOf_X_self_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Nontrivial R] (i : σ) (k : ℕ) :

degreeOf i (X i ^ k) = k

theorem MvPolynomial.degreeOf_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (k : ℕ) (h : i ≠ j) :

degreeOf i (X j ^ k) = 0

@[simp]

theorem MvPolynomial.degreeOf_X_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Nontrivial R] (i : σ) :

degreeOf i (X i) = 1

theorem MvPolynomial.degreeOf_X_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (h : i ≠ j) :

degreeOf i (X j) = 0

theorem MvPolynomial.degreeOf_mul_X_self_pow_eq_add_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) (k : ℕ) (h : p ≠ 0) :

degreeOf i (p * X i ^ k) = degreeOf i p + k

theorem MvPolynomial.degreeOf_mul_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i j : σ} (k : ℕ) (h : i ≠ j) :

degreeOf i (p * X j ^ k) = degreeOf i p

theorem MvPolynomial.degreeOf_add_eq_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} {i : σ} (h : degreeOf i q < degreeOf i p) :

degreeOf i (p + q) = degreeOf i p

theorem MvPolynomial.degreeOf_eq_of_degreeOf_add_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q : MvPolynomial σ R} (h : degreeOf i (p + q) < degreeOf i p) :

degreeOf i p = degreeOf i q

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

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

Equations

p.mainDegree = match p.mainVariable with | none => 0 | some c => MvPolynomial.degreeOf c p

Instances For

theorem MvPolynomial.mainDegree_of_mainVariable_isSome {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} :

p.mainVariable = ↑c → p.mainDegree = degreeOf c p

theorem MvPolynomial.mainDegree_of_mainVariable_isSome' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} :

p.mainVariable = ↑c → p.mainDegree = p.support.sup fun (s : σ →₀ ℕ) => s c

theorem MvPolynomial.mainDegree_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] :

p.mainDegree = 0 ↔ p.mainVariable = ⊥

theorem MvPolynomial.mainDegree_eq_zero_iff' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] :

p.mainDegree = 0 ↔ ∃ (r : R), p = C r

theorem MvPolynomial.degreeOf_mainVariable_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} :

p.mainVariable = ↑c → degreeOf c p ≠ 0

theorem MvPolynomial.mainVariable_mem_degrees {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] {c : σ} :

p.mainVariable = ↑c → c ∈ p.degrees

@[simp]

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

mainDegree 0 = 0

@[simp]

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

((monomial s) r).mainDegree = s c

@[simp]

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

(C r).mainDegree = 0

@[simp]

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

(X i ^ k).mainDegree = k

@[simp]

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

(X i).mainDegree = 1

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

Lex (WithBot σ × ℕ)

The rank of a polynomial p is the pair (mainVariable p, degree p). Ranks are ordered lexicographically.

Equations

p.rank = (p.mainVariable, p.mainDegree)

Instances For

theorem MvPolynomial.rank_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} :

p.rank = (p.mainVariable, p.mainDegree)

theorem MvPolynomial.rank_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p.rank = q.rank ↔ p.mainVariable = q.mainVariable ∧ p.mainDegree = q.mainDegree

instance MvPolynomial.instPreorder {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

Preorder (MvPolynomial σ R)

Equations

MvPolynomial.instPreorder = { le := InvImage (fun (x1 x2 : Lex (WithBot σ × ℕ)) => x1 ≤ x2) MvPolynomial.rank, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem MvPolynomial.le_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q ↔ p.rank ≤ q.rank

noncomputable instance MvPolynomial.instDecidableLE {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

DecidableLE (MvPolynomial σ R)

Equations

x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.rank ≤ x✝.rank) ⋯

noncomputable instance MvPolynomial.instDecidableLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

DecidableLT (MvPolynomial σ R)

Equations

MvPolynomial.instDecidableLT = decidableLTOfDecidableLE

instance MvPolynomial.instIsTotalLe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

Std.Total LE.le

theorem MvPolynomial.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q ↔ p.mainVariable < q.mainVariable ∨ p.mainVariable = q.mainVariable ∧ p.mainDegree ≤ q.mainDegree

theorem MvPolynomial.le_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q ↔ ¬p.mainVariable < q.mainVariable → p.mainVariable = q.mainVariable ∧ p.mainDegree ≤ q.mainDegree

theorem MvPolynomial.mainVariable_le_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q → p.mainVariable ≤ q.mainVariable

theorem MvPolynomial.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p < q ↔ p.rank < q.rank

theorem MvPolynomial.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p < q ↔ p.mainVariable < q.mainVariable ∨ p.mainVariable = q.mainVariable ∧ p.mainDegree < q.mainDegree

theorem MvPolynomial.lt_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p < q ↔ ¬p.mainVariable < q.mainVariable → p.mainVariable = q.mainVariable ∧ p.mainDegree < q.mainDegree

theorem MvPolynomial.lt_of_mainVariable_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p.mainVariable < q.mainVariable → p < q

@[simp]

theorem MvPolynomial.not_lt_iff_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

¬p < q ↔ q ≤ p

@[simp]

theorem MvPolynomial.not_le_iff_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

¬p ≤ q ↔ q < p

theorem MvPolynomial.X_lt_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] {i j : σ} :

i < j → X i < X j

instance MvPolynomial.instSetoid {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

Setoid (MvPolynomial σ R)

Equations

MvPolynomial.instSetoid = AntisymmRel.setoid (MvPolynomial σ R) fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2

noncomputable instance MvPolynomial.instDecidableRelEquiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

DecidableRel fun (x1 x2 : MvPolynomial σ R) => x1 ≈ x2

Equations

x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem MvPolynomial.equiv_def'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≈ q ↔ p ≤ q ∧ q ≤ p

theorem MvPolynomial.equiv_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≈ q ↔ p.rank = q.rank

theorem MvPolynomial.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≈ q ↔ ¬p < q ∧ ¬q < p

theorem MvPolynomial.equiv_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≈ q ↔ p.mainVariable = q.mainVariable ∧ p.mainDegree = q.mainDegree

theorem MvPolynomial.le_iff_lt_or_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q ↔ p < q ∨ p ≈ q

theorem MvPolynomial.lt_of_equiv_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p r : MvPolynomial σ R} :

p ≈ q → q < r → p < r

theorem MvPolynomial.lt_of_lt_of_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p r : MvPolynomial σ R} :

p < q → q ≈ r → p < r

theorem MvPolynomial.equiv_of_le_of_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] {q : MvPolynomial σ R} [LinearOrder σ] {p : MvPolynomial σ R} :

p ≤ q → q ≤ p → p ≈ q

theorem MvPolynomial.zero_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} :

0 ≤ p

theorem MvPolynomial.wellFoundedLT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] :

WellFoundedLT (MvPolynomial σ R) → WellFoundedLT σ

instance MvPolynomial.instWellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT σ] :

WellFoundedLT (MvPolynomial σ R)

theorem MvPolynomial.wellFoundedLT_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] :

WellFoundedLT (MvPolynomial σ R) ↔ WellFoundedLT σ

theorem MvPolynomial.Set.has_min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) :

∃ p ∈ PS, ∀ q ∈ PS, ¬q < p

noncomputable def MvPolynomial.Set.min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) :

MvPolynomial σ R

Equations

MvPolynomial.Set.min PS h = ⋯.choose

Instances For

theorem MvPolynomial.Set.min_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) :

min PS h ∈ PS

def MvPolynomial.reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (q p : MvPolynomial σ R) :

q is reduced with respect to pif q = 0 or if the degree of q in the main variable of p is strictly less than the degree of p.

Note: if p is a constant, then no non-zero q is reduced with respect to p.

Equations

q.reducedTo p = if q = 0 then True else match p.mainVariable with | none => False | some c => MvPolynomial.degreeOf c q < MvPolynomial.degreeOf c p

Instances For

theorem MvPolynomial.zero_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (p : MvPolynomial σ R) :

theorem MvPolynomial.not_reducedTo_of_bot_mainVariable {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) :

p.mainVariable = ⊥ → ¬q.reducedTo p

theorem MvPolynomial.mainVariable_ne_bot_of_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) :

q.reducedTo p → p.mainVariable ≠ ⊥

theorem MvPolynomial.reducedTo_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} {c : σ} (hp : p.mainVariable = ↑c) (hq : q ≠ 0) :

q.reducedTo p ↔ degreeOf c q < degreeOf c p

noncomputable instance MvPolynomial.instDecidableRelReducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] :

DecidableRel reducedTo

Equations

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

theorem MvPolynomial.reducedTo_of_mainVariable_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h : q.mainVariable < p.mainVariable) :

theorem MvPolynomial.reducedTo_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q r : MvPolynomial σ R} :

p ≈ q → (r.reducedTo p ↔ r.reducedTo q)

theorem MvPolynomial.reducedTo_iff_gt_of_mainVariable_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) (h : q.mainVariable = p.mainVariable) :

q.reducedTo p ↔ q < p

theorem MvPolynomial.not_reduceTo_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (h : p ≠ 0) :

¬p.reducedTo p

theorem MvPolynomial.mainVariable_lt_of_reducedTo_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h1 : q ≠ 0) (h2 : p ≤ q) (h3 : q.reducedTo p) :

p.mainVariable < q.mainVariable

theorem MvPolynomial.lt_of_reducedTo_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h1 : q ≠ 0) (h2 : p ≤ q) (h3 : q.reducedTo p) :

p < q

def MvPolynomial.reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (q : MvPolynomial σ R) (a : α) :

q is reduced with respect to a set a if it is reduced with respect to all elements of a.

Equations

q.reducedToSet a = ∀ p ∈ a, q.reducedTo p

Instances For

noncomputable instance MvPolynomial.instDecidableRelListReducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] :

DecidableRel reducedToSet

Equations

x✝.instDecidableRelListReducedToSet = List.decidableBAll x✝.reducedTo

theorem MvPolynomial.reducedToSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] {q : MvPolynomial σ R} {a : α} :

q.reducedToSet a ↔ ∀ p ∈ a, q.reducedTo p

theorem MvPolynomial.zero_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] {a : α} :

reducedToSet 0 a