@[simp]

theorem HexMvPolyMathlib.support_toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : (toMvPolynomial p).support = Finset.map monoEquiv.toEmbedding p.monomials.toFinset

The Mathlib support is exactly the image of the executable canonical support.

@[simp]

theorem HexMvPolyMathlib.degreeOf_toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (i : Fin n) (p : Hex.MvPoly n R cmp) : Hex.MvPoly.degreeOf i p = MvPolynomial.degreeOf i (toMvPolynomial p)

Executable per-variable degree agrees with Mathlib's degreeOf.

@[simp]

theorem HexMvPolyMathlib.get_degrees_eq_degreeOf {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (i : Fin n) (p : Hex.MvPoly n R cmp) : p.degrees[i] = MvPolynomial.degreeOf i (toMvPolynomial p)

Each executable coordinate degree is Mathlib's corresponding per-variable degree.

@[simp]

theorem HexMvPolyMathlib.mem_vars_iff_degreeOf {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (i : Fin n) (p : Hex.MvPoly n R cmp) : i ∈ p.vars ↔ MvPolynomial.degreeOf i (toMvPolynomial p) ≠ 0

The executable variable list contains exactly the variables of nonzero Mathlib degree.

theorem HexMvPolyMathlib.monoDegree_eq_sum {n : ℕ} (m : Hex.Mono n) : m.degree = (monoEquiv m).sum fun (x : Fin n) (e : ℕ) => e

Total exponent in an executable monomial is the corresponding Finsupp sum.

@[simp]

theorem HexMvPolyMathlib.totalDegree_toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : p.totalDegree = (toMvPolynomial p).totalDegree

Executable total degree agrees with Mathlib's totalDegree.

theorem HexMvPolyMathlib.evalHorner_eq_aeval {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (x : Fin n → R) (p : Hex.MvPoly n R cmp) : Hex.MvPoly.evalHorner x p = (MvPolynomial.aeval x) (toMvPolynomial p)

Fixed-order Horner evaluation has the same Mathlib interpretation as direct algebra-hom evaluation.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_succAt {n : ℕ} (i : Fin n) (m : Hex.Mono n) : monoEquiv (Hex.Mono.succAt i m) = monoEquiv m + Finsupp.single i 1

Increasing one executable exponent corresponds to adding the Mathlib single-variable exponent.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_derivative {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (i : Fin n) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.derivative i p) = (MvPolynomial.pderiv i) (toMvPolynomial p)

Executable formal differentiation agrees with Mathlib's partial derivative.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_homogeneousComponent {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (d : ℕ) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.homogeneousComponent d p) = (MvPolynomial.homogeneousComponent d) (toMvPolynomial p)

Executable homogeneous projection agrees with Mathlib's homogeneous component.

theorem HexMvPolyMathlib.subst_eq_aeval {n k : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [CommSemiring R] [DecidableEq R] (g : Fin n → Hex.MvPoly k R targetCmp) (p : Hex.MvPoly n R cmp) : Hex.MvPoly.subst g p = (aeval g) p

Executable substitution is its algebra-hom evaluation specialization.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_subst {n k : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [CommSemiring R] [DecidableEq R] (g : Fin n → Hex.MvPoly k R targetCmp) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.subst g p) = (MvPolynomial.bind₁ fun (i : Fin n) => toMvPolynomial (g i)) (toMvPolynomial p)

Executable substitution agrees with Mathlib's variable bind.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_partialEval {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (s : Fin n → Option R) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.partialEval s p) = (MvPolynomial.bind₁ fun (i : Fin n) => match s i with | some x => MvPolynomial.C x | none => MvPolynomial.X i) (toMvPolynomial p)

Executable partial evaluation agrees with binding assigned variables to constants and leaving the other variables unchanged.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_bind₁ {n k : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [CommSemiring R] [DecidableEq R] (g : Fin n → Hex.MvPoly k R targetCmp) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.bind₁ g p) = (MvPolynomial.bind₁ fun (i : Fin n) => toMvPolynomial (g i)) (toMvPolynomial p)

The compatibility spelling bind₁ has the same Mathlib correspondence as substitution.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_reorder {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.reorder cmp' p) = toMvPolynomial p

Changing the executable storage order does not change the corresponding Mathlib polynomial.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_rename {n k : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp] [Std.LawfulEqCmp targetCmp] [CommSemiring R] [DecidableEq R] (f : Fin n → Fin k) (p : Hex.MvPoly n R cmp) : toMvPolynomial (Hex.MvPoly.rename targetCmp f p) = (MvPolynomial.rename f) (toMvPolynomial p)

Executable variable renaming agrees with Mathlib's rename.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_ofUnivariate {n : ℕ} {R : Type u} {cmpSucc : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmpBase : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmpSucc] [Std.LawfulEqCmp cmpSucc] [Std.TransCmp cmpBase] [Std.LawfulEqCmp cmpBase] [CommSemiring R] [DecidableEq R] (q : Hex.DensePoly (Hex.MvPoly n R cmpBase)) : toMvPolynomial (Hex.MvPoly.ofUnivariate 0 cmpBase q) = (MvPolynomial.finSuccEquiv R n).symm (recursiveMap q)

The inverse executable recursive view agrees with the inverse Mathlib finSuccEquiv.