HexMvPolyMathlib.Recursive

@[simp]

theorem HexMvPolyMathlib.monoEquiv_insertZero {n : ℕ} (e : ℕ) (m : Hex.Mono n) :

monoEquiv (Hex.MvPoly.insertVar 0 e m) = Finsupp.cons e (monoEquiv m)

Inserting the main-variable exponent corresponds to adding its Mathlib single term to the shifted remaining exponents.

noncomputable def HexMvPolyMathlib.recursiveMap {n : ℕ} {R : Type u} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] (q : Hex.DensePoly (Hex.MvPoly n R cmp')) :

Polynomial (MvPolynomial (Fin n) R)

Send the executable recursive view through the two exact representation bridges, obtaining a Mathlib polynomial over Mathlib multivariate polynomials.

Equations

HexMvPolyMathlib.recursiveMap q = Polynomial.map HexMvPolyMathlib.equiv.toRingHom (HexPolyMathlib.toPolynomial q)

Instances For

source

@[simp]

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

recursiveMap (Hex.MvPoly.toUnivariate 0 cmp' p) = (MvPolynomial.finSuccEquiv R n) (toMvPolynomial p)

The executable recursive view agrees exactly with Mathlib's MvPolynomial.finSuccEquiv.

source

theorem HexMvPolyMathlib.recursiveMap_injective {n : ℕ} {R : Type u} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] :

Function.Injective recursiveMap

The composite comparison map for the recursive view is injective.

source

@[simp]

theorem HexMvPolyMathlib.recursiveMap_zero {n : ℕ} {R : Type u} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] :

recursiveMap 0 = 0

The comparison map preserves zero.

source

@[simp]

theorem HexMvPolyMathlib.recursiveMap_one {n : ℕ} {R : Type u} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] :

recursiveMap 1 = 1

The comparison map preserves one.

source

@[simp]

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

recursiveMap (p + q) = recursiveMap p + recursiveMap q

The comparison map preserves addition.

source

@[simp]

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

recursiveMap (p * q) = recursiveMap p * recursiveMap q

The comparison map preserves multiplication.

source

@[simp]

theorem HexMvPolyMathlib.toUnivariate_zero {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] :

Hex.MvPoly.toUnivariate 0 cmp' 0 = 0

The recursive view preserves zero.

source

@[simp]

theorem HexMvPolyMathlib.toUnivariate_one {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] :

Hex.MvPoly.toUnivariate 0 cmp' 1 = 1

The recursive view preserves one.

source

@[simp]

theorem HexMvPolyMathlib.toUnivariate_add {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] (p q : Hex.MvPoly (n + 1) R cmp) :

Hex.MvPoly.toUnivariate 0 cmp' (p + q) = Hex.MvPoly.toUnivariate 0 cmp' p + Hex.MvPoly.toUnivariate 0 cmp' q

The recursive view preserves addition.

source

@[simp]

theorem HexMvPolyMathlib.toUnivariate_mul {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] (p q : Hex.MvPoly (n + 1) R cmp) :

Hex.MvPoly.toUnivariate 0 cmp' (p * q) = Hex.MvPoly.toUnivariate 0 cmp' p * Hex.MvPoly.toUnivariate 0 cmp' q

The recursive view preserves multiplication.

source

def HexMvPolyMathlib.finSuccEquiv {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → 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'] :

Hex.MvPoly (n + 1) R cmp ≃+* Hex.DensePoly (Hex.MvPoly n R cmp')

The executable recursive view at the first variable, packaged as a ring equivalence.

Equations

HexMvPolyMathlib.finSuccEquiv cmp' = { toFun := Hex.MvPoly.toUnivariate 0 cmp', invFun := Hex.MvPoly.ofUnivariate 0 cmp', left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

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

(finSuccEquiv cmp') p = Hex.MvPoly.toUnivariate 0 cmp' p

The finite-successor ring equivalence applies as the recursive view.

source

@[simp]

theorem HexMvPolyMathlib.finSuccEquiv_symm_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering} {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [CommSemiring R] [DecidableEq R] (q : Hex.DensePoly (Hex.MvPoly n R cmp')) :

(finSuccEquiv cmp').symm q = Hex.MvPoly.ofUnivariate 0 cmp' q

The inverse finite-successor ring equivalence applies as recursive-view reassembly.

source

noncomputable def HexMvPolyMathlib.isEmptyRingEquiv {R : Type u} {cmp0 : Hex.Mono 0 → Hex.Mono 0 → Ordering} [Std.TransCmp cmp0] [Std.LawfulEqCmp cmp0] [CommSemiring R] [DecidableEq R] :

Hex.MvPoly 0 R cmp0 ≃+* R

Arity zero has only the constant monomial.

Equations

HexMvPolyMathlib.isEmptyRingEquiv = HexMvPolyMathlib.equiv.trans (MvPolynomial.isEmptyRingEquiv R (Fin 0))

Instances For

source

@[simp]

theorem HexMvPolyMathlib.isEmptyRingEquiv_apply {R : Type u} {cmp0 : Hex.Mono 0 → Hex.Mono 0 → Ordering} [Std.TransCmp cmp0] [Std.LawfulEqCmp cmp0] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly 0 R cmp0) :

isEmptyRingEquiv p = Hex.MvPoly.coeff Hex.Mono.zero p

The zero-variable equivalence reads the constant coefficient.

source

@[simp]

theorem HexMvPolyMathlib.isEmptyRingEquiv_symm_apply {R : Type u} {cmp0 : Hex.Mono 0 → Hex.Mono 0 → Ordering} [Std.TransCmp cmp0] [Std.LawfulEqCmp cmp0] [CommSemiring R] [DecidableEq R] (r : R) :

isEmptyRingEquiv.symm r = Hex.MvPoly.C r

The inverse zero-variable equivalence builds a constant polynomial.

source

noncomputable def HexMvPolyMathlib.oneVarEquiv {R : Type u} {cmp1 : Hex.Mono 1 → Hex.Mono 1 → Ordering} [Std.TransCmp cmp1] [Std.LawfulEqCmp cmp1] [CommSemiring R] [DecidableEq R] :

Hex.MvPoly 1 R cmp1 ≃+* Hex.DensePoly R

A one-variable executable multivariate polynomial is a dense univariate polynomial.

Equations

HexMvPolyMathlib.oneVarEquiv = (HexMvPolyMathlib.finSuccEquiv Hex.Mono.lex).trans (HexPolyMathlib.mapEquiv HexMvPolyMathlib.isEmptyRingEquiv)

Instances For

source

@[simp]

theorem HexMvPolyMathlib.oneVarEquiv_apply {R : Type u} {cmp1 : Hex.Mono 1 → Hex.Mono 1 → Ordering} [Std.TransCmp cmp1] [Std.LawfulEqCmp cmp1] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly 1 R cmp1) :

oneVarEquiv p = (HexPolyMathlib.mapEquiv isEmptyRingEquiv) (Hex.MvPoly.toUnivariate 0 Hex.Mono.lex p)

The one-variable equivalence applies as the recursive view with constant coefficient polynomials identified with coefficients.

source

@[simp]

theorem HexMvPolyMathlib.oneVarEquiv_symm_apply {R : Type u} {cmp1 : Hex.Mono 1 → Hex.Mono 1 → Ordering} [Std.TransCmp cmp1] [Std.LawfulEqCmp cmp1] [CommSemiring R] [DecidableEq R] (q : Hex.DensePoly R) :

oneVarEquiv.symm q = Hex.MvPoly.ofUnivariate 0 Hex.Mono.lex ((HexPolyMathlib.mapEquiv isEmptyRingEquiv).symm q)

The inverse one-variable equivalence reassembles a dense polynomial.