def Hex.MvPoly.reorder {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (cmp' : Mono n → Mono n → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) : MvPoly n R cmp'

Rebuild a polynomial under a different monomial comparator.

Equations

• Hex.MvPoly.reorder cmp' p = Hex.MvPoly.ofTerms p.termsList

def Hex.MvPoly.rename {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (cmp' : Mono k → Mono k → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [Lean.Grind.Semiring R] [DecidableEq R] (f : Fin n → Fin k) (p : MvPoly n R cmp) : MvPoly k R cmp'

Rename variables, adding exponents in fibres and combining all resulting term collisions.

Equations

• Hex.MvPoly.rename cmp' f p = Hex.MvPoly.foldTerms (fun (acc : Hex.MvPoly k R cmp') (m : Hex.Mono n) (c : R) => acc.addMonomial (Hex.Mono.rename f m) c) 0 p

def Hex.MvPoly.predAt {n : Nat} (i : Fin n) (m : Mono n) : Mono n

Decrease the exponent at i by one, leaving every other exponent unchanged.

Equations

• Hex.MvPoly.predAt i m = Hex.Vector.ofFn' fun (j : Fin n) => if j = i then m[j] - 1 else m[j]

@[simp]

theorem Hex.MvPoly.degreeOf_succAt {n : Nat} (i : Fin n) (m : Mono n) : Mono.degreeOf i (Mono.succAt i m) = Mono.degreeOf i m + 1

Incrementing a monomial raises the selected variable degree by one.

@[simp]

theorem Hex.MvPoly.predAt_succAt {n : Nat} (i : Fin n) (m : Mono n) : predAt i (Mono.succAt i m) = m

Decrementing the selected exponent reverses succAt.

theorem Hex.MvPoly.predAt_eq_iff {n : Nat} (i : Fin n) (m t : Mono n) (ht : Mono.degreeOf i t ≠ 0) : predAt i t = m ↔ t = Mono.succAt i m

predAt yields a monomial exactly when the source is its successor at the selected variable.

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

Formal derivative with respect to variable i.

Equations

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

def Hex.MvPoly.homogeneousComponent {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (d : Nat) (p : MvPoly n R cmp) : MvPoly n R cmp

Homogeneous component of total degree d.

Equations

• Hex.MvPoly.homogeneousComponent d p = Hex.MvPoly.restrictBy (fun (m : Hex.Mono n) => decide (m.degree = d)) p

def Hex.MvPoly.bind {n k : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Zero R] [Lean.Grind.Semiring S] [DecidableEq S] (f : R → S) (g : Fin n → MvPoly k S targetCmp) (p : MvPoly n R cmp) : MvPoly k S targetCmp

General substitution, mapping coefficients through f and variables through g.

Equations

• Hex.MvPoly.bind f g p = Hex.MvPoly.foldTerms (fun (acc : Hex.MvPoly k S targetCmp) (m : Hex.Mono n) (c : R) => acc + Hex.MvPoly.C (f c) * Hex.Mono.prod g m) 0 p

theorem Hex.MvPoly.bind_eq {n k : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Zero R] [Lean.Grind.Semiring S] [DecidableEq S] (f : R → S) (g : Fin n → MvPoly k S targetCmp) (p : MvPoly n R cmp) : bind f g p = List.foldl (fun (acc : MvPoly k S targetCmp) (term : Mono n × R) => acc + C (f term.snd) * Mono.prod g term.fst) 0 p.termsList

General substitution is the ordered sum of mapped coefficient-monomial terms.

def Hex.MvPoly.subst {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Lean.Grind.Semiring R] [DecidableEq R] (f : Fin n → MvPoly k R targetCmp) (p : MvPoly n R cmp) : MvPoly k R targetCmp

Substitute polynomials for variables without changing the coefficient type.

Equations

• Hex.MvPoly.subst f p = Hex.MvPoly.bind id f p

def Hex.MvPoly.bind₁ {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Lean.Grind.Semiring R] [DecidableEq R] (f : Fin n → MvPoly k R targetCmp) (p : MvPoly n R cmp) : MvPoly k R targetCmp

Compatibility spelling for same-coefficient substitution.

Equations

• Hex.MvPoly.bind₁ f p = Hex.MvPoly.subst f p

def Hex.MvPoly.sumToIter {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) : MvPoly n R cmp

Reconstruct a polynomial by summing its ordered term iteration.

Equations

• p.sumToIter = Hex.MvPoly.ofTerms p.termsList

@[simp]

theorem Hex.MvPoly.sumToIter_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) : p.sumToIter = p

Reconstructing from the ordered term iterator recovers the polynomial.

theorem Hex.MvPoly.coeff_reorder {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (cmp' : Mono n → Mono n → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (m : Mono n) (p : MvPoly n R cmp) : coeff m (reorder cmp' p) = coeff m p

Reordering a polynomial preserves every coefficient.

theorem Hex.MvPoly.coeff_rename {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (cmp' : Mono k → Mono k → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (f : Fin n → Fin k) (m : Mono k) (p : MvPoly n R cmp) : coeff m (rename cmp' f p) = List.foldl (fun (acc : R) (term : Mono n × R) => if Mono.rename f term.fst = m then acc + term.snd else acc) 0 p.termsList

Renaming variables sums coefficients whose target monomials coincide.

theorem Hex.MvPoly.coeff_derivative {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin n) (m : Mono n) (p : MvPoly n R cmp) : coeff m (derivative i p) = ↑(Mono.degreeOf i m + 1) * coeff (Mono.succAt i m) p

A derivative coefficient is the successor coefficient scaled by its corresponding exponent.

theorem Hex.MvPoly.coeff_homogeneousComponent {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (d : Nat) (m : Mono n) (p : MvPoly n R cmp) : coeff m (homogeneousComponent d p) = if m.degree = d then coeff m p else 0

A homogeneous component keeps exactly the terms of the requested total degree.

theorem Hex.MvPoly.subst_eq {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Lean.Grind.Semiring R] [DecidableEq R] (f : Fin n → MvPoly k R targetCmp) (p : MvPoly n R cmp) : subst f p = List.foldl (fun (acc : MvPoly k R targetCmp) (term : Mono n × R) => acc + C term.snd * Mono.prod f term.fst) 0 p.termsList

Substitution evaluates each source monomial at the replacement polynomials and sums the results.

theorem Hex.MvPoly.rename_eq_subst {n k : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} {targetCmp : Mono k → Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [Lean.Grind.Semiring R] [DecidableEq R] (f : Fin n → Fin k) (p : MvPoly n R cmp) : rename targetCmp f p = subst (fun (i : Fin n) => X (f i)) p

Renaming is substitution by the target variables.

theorem Hex.MvPoly.partialEval_eq_subst {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (s : Fin n → Option R) (p : MvPoly n R cmp) : partialEval s p = subst (fun (i : Fin n) => match s i with | some x => C x | none => X i) p

Partial evaluation is substitution by constants at assigned variables and variables at unassigned ones.