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.reorder_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (p q : MvPoly n R cmp) : reorder cmp' (p * q) = reorder cmp' p * reorder cmp' q

Reordering preserves multiplication while changing only the term order.

theorem Hex.MvPoly.reorder_one {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] : reorder cmp' 1 = 1

Reordering preserves the multiplicative identity.

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.

def Hex.MvPoly.mapCoeffs {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Zero S] [BEq S] [LawfulBEq S] (φ : R → S) (p : MvPoly n R cmp) : MvPoly n S cmp

Map φ over the coefficients, dropping every term it sends to zero.

Terms are never merged, since the monomials are untouched, so this is the one member of the substitution family that cannot create a collision.

Equations

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

@[simp]

theorem Hex.MvPoly.coeff_mapCoeffs {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Zero S] [BEq S] [LawfulBEq S] {φ : R → S} (hzero : φ 0 = 0) (m : Mono n) (p : MvPoly n R cmp) : coeff m (mapCoeffs φ p) = φ (coeff m p)

Coefficients of a coefficient map, for a φ that fixes zero.

theorem Hex.MvPoly.mapCoeffs_zero {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [Lean.Grind.Semiring S] [BEq S] [LawfulBEq S] {φ : R → S} (hzero : φ 0 = 0) : mapCoeffs φ 0 = 0

A coefficient map fixing zero sends the zero polynomial to zero.

theorem Hex.MvPoly.mapCoeffs_one {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring S] [DecidableEq S] [BEq S] [LawfulBEq S] {φ : R → S} (hzero : φ 0 = 0) (hone : φ 1 = 1) : mapCoeffs φ 1 = 1

A coefficient map fixing zero and one sends one to one.

theorem Hex.MvPoly.mapCoeffs_add {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring S] [DecidableEq S] [BEq S] [LawfulBEq S] {φ : R → S} (hzero : φ 0 = 0) (hadd : ∀ (a b : R), φ (a + b) = φ a + φ b) (p q : MvPoly n R cmp) : mapCoeffs φ (p + q) = mapCoeffs φ p + mapCoeffs φ q

An additive coefficient map commutes with polynomial addition.

theorem Hex.MvPoly.mapCoeffs_mul {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring S] [DecidableEq S] [BEq S] [LawfulBEq S] {φ : R → S} (hzero : φ 0 = 0) (hadd : ∀ (a b : R), φ (a + b) = φ a + φ b) (hmul : ∀ (a b : R), φ (a * b) = φ a * φ b) (p q : MvPoly n R cmp) : mapCoeffs φ (p * q) = mapCoeffs φ p * mapCoeffs φ q

A ring map on coefficients commutes with polynomial multiplication.