def Hex.MvPoly.totalDegree {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : Nat

Maximum total degree of a supported monomial, or zero for the zero polynomial.

Equations

• p.totalDegree = Hex.MvPoly.foldTerms (fun (d : Nat) (m : Hex.Mono n) (x : R) => max d m.degree) 0 p

def Hex.MvPoly.degreeOf {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) (p : MvPoly n R cmp) : Nat

Maximum exponent of variable i, or zero for the zero polynomial.

Equations

• Hex.MvPoly.degreeOf i p = Hex.MvPoly.foldTerms (fun (d : Nat) (m : Hex.Mono n) (x : R) => max d (Hex.Mono.degreeOf i m)) 0 p

theorem Hex.MvPoly.totalDegree_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : p.totalDegree = foldTerms (fun (d : Nat) (m : Mono n) (x : R) => max d m.degree) 0 p

Total degree is the maximum monomial degree in ordered term iteration.

theorem Hex.MvPoly.degreeOf_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) (p : MvPoly n R cmp) : degreeOf i p = foldTerms (fun (d : Nat) (m : Mono n) (x : R) => max d (Mono.degreeOf i m)) 0 p

Per-variable degree is the maximum exponent in ordered term iteration.

def Hex.MvPoly.degrees {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : Mono n

Coordinatewise maximum of all supported exponent vectors.

Equations

• p.degrees = Hex.MvPoly.foldTerms (fun (d m : Hex.Mono n) (x : R) => d.lcm m) Hex.Mono.zero p

theorem Hex.MvPoly.degrees_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : p.degrees = foldTerms (fun (d m : Mono n) (x : R) => d.lcm m) Mono.zero p

The coordinatewise degree vector is a fold over the canonical terms.

@[simp]

theorem Hex.MvPoly.getElem_degrees {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) (i : Fin n) : p.degrees[i] = degreeOf i p

Each coordinate of degrees is the corresponding per-variable degree.

def Hex.MvPoly.vars {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : List (Fin n)

Variables occurring in at least one supported monomial, in increasing index order.

Equations

• p.vars = p.degrees.support

theorem Hex.MvPoly.vars_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : p.vars = p.degrees.support

Variables are the support of the coordinatewise degree vector.

@[simp]

theorem Hex.MvPoly.mem_vars_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) (p : MvPoly n R cmp) : i ∈ p.vars ↔ degreeOf i p ≠ 0

A variable occurs exactly when its maximum exponent is nonzero.

def Hex.MvPoly.leadingTerm {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : Option (Mono n × R)

Greatest supported term in the polynomial's monomial order.

Equations

• p.leadingTerm = p.maxTerm?

theorem Hex.MvPoly.leadingTerm_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : p.leadingTerm = p.maxTerm?

The leading term is the maximum entry of the canonical term map.

theorem Hex.MvPoly.leadingTerm_eq_some_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) (m : Mono n) (c : R) : p.leadingTerm = some (m, c) ↔ coeff? m p = some c ∧ ∀ (k : Mono n), k ∈ p.monomials → (cmp k m).isLE = true

A leading term is exactly a stored coefficient whose monomial bounds every monomial in the canonical support.

theorem Hex.MvPoly.coeff_eq_of_leadingTerm {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] {p : MvPoly n R cmp} {m : Mono n} {c : R} (h : p.leadingTerm = some (m, c)) : coeff m p = c

The coefficient recorded by a leading term is the public coefficient at its monomial.

theorem Hex.MvPoly.le_leadingTerm {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] {p : MvPoly n R cmp} {m : Mono n} {c : R} (h : p.leadingTerm = some (m, c)) (k : Mono n) : k ∈ p.monomials → (cmp k m).isLE = true

Every supported monomial is at most the leading monomial.

def Hex.MvPoly.leadingMono {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : Option (Mono n)

Greatest supported monomial in the polynomial's monomial order.

Equations

• p.leadingMono = Option.map Prod.fst p.leadingTerm

theorem Hex.MvPoly.leadingMono_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : p.leadingMono = Option.map Prod.fst p.leadingTerm

The leading monomial is the monomial projection of the leading term.

def Hex.MvPoly.leadingMonomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : Option (Mono n)

Compatibility spelling for leadingMono.

Equations

• p.leadingMonomial = p.leadingMono

theorem Hex.MvPoly.leadingMonomial_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : p.leadingMonomial = p.leadingMono

The compatibility spelling agrees with leadingMono.

def Hex.MvPoly.leadingCoeff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : R

Coefficient of the greatest supported monomial, or zero for the zero polynomial.

Equations

• p.leadingCoeff = match p.leadingTerm with | none => 0 | some term => term.snd

theorem Hex.MvPoly.leadingCoeff_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] (p : MvPoly n R cmp) : p.leadingCoeff = (Option.map Prod.snd p.leadingTerm).getD 0

The leading coefficient is the coefficient projection of the leading term, defaulting to zero.

def Hex.MvPoly.restrictBy {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (keep : Mono n → Bool) (p : MvPoly n R cmp) : MvPoly n R cmp

Retain exactly the terms whose monomials satisfy keep.

Equations

• Hex.MvPoly.restrictBy keep p = { termsInternal := Std.ExtTreeMap.filter (fun (m : Hex.Mono n) (x : R) => keep m) p.termsInternal, nonzeroInternal := ⋯ }

def Hex.MvPoly.restrictDegree {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) (bound : Nat) (p : MvPoly n R cmp) : MvPoly n R cmp

Retain the terms whose exponent of i is at most bound.

Equations

• Hex.MvPoly.restrictDegree i bound p = Hex.MvPoly.restrictBy (fun (m : Hex.Mono n) => decide (Hex.Mono.degreeOf i m ≤ bound)) p

theorem Hex.MvPoly.restrictDegree_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) (bound : Nat) (p : MvPoly n R cmp) : restrictDegree i bound p = restrictBy (fun (m : Mono n) => decide (Mono.degreeOf i m ≤ bound)) p

Per-variable restriction is restriction by the corresponding exponent bound.

def Hex.MvPoly.restrictTotalDegree {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (bound : Nat) (p : MvPoly n R cmp) : MvPoly n R cmp

Retain the terms whose total degree is at most bound.

Equations

• Hex.MvPoly.restrictTotalDegree bound p = Hex.MvPoly.restrictBy (fun (m : Hex.Mono n) => decide (m.degree ≤ bound)) p

theorem Hex.MvPoly.restrictTotalDegree_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (bound : Nat) (p : MvPoly n R cmp) : restrictTotalDegree bound p = restrictBy (fun (m : Mono n) => decide (m.degree ≤ bound)) p

Total-degree restriction is restriction by the monomial degree bound.

theorem Hex.MvPoly.coeff_restrictBy {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (keep : Mono n → Bool) (m : Mono n) (p : MvPoly n R cmp) : coeff m (restrictBy keep p) = if keep m = true then coeff m p else 0

Restriction keeps exactly the coefficients whose monomials satisfy the predicate.

@[simp]

theorem Hex.MvPoly.totalDegree_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : totalDegree 0 = 0

The zero polynomial has total degree zero.

@[simp]

theorem Hex.MvPoly.degreeOf_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (i : Fin n) : degreeOf i 0 = 0

Every variable has degree zero in the zero polynomial.

@[simp]

theorem Hex.MvPoly.degrees_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : degrees 0 = Mono.zero

The coordinatewise degree vector of zero is the zero monomial.

@[simp]

theorem Hex.MvPoly.vars_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : vars 0 = []

No variable occurs in the zero polynomial.

@[simp]

theorem Hex.MvPoly.leadingTerm_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] : leadingTerm 0 = none

The zero polynomial has no leading term.

@[simp]

theorem Hex.MvPoly.leadingMono_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] : leadingMono 0 = none

The zero polynomial has no leading monomial.

@[simp]

theorem Hex.MvPoly.leadingMonomial_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] : leadingMonomial 0 = none

The compatibility leading-monomial spelling returns none on zero.

@[simp]

theorem Hex.MvPoly.leadingCoeff_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [IsMonomialOrder cmp] : leadingCoeff 0 = 0

The zero polynomial has leading coefficient zero.