noncomputable def HexMvPolyMathlib.aevalMathlib {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) : Hex.MvPoly n R cmp →ₐ[R] S

Auxiliary Mathlib-transported algebra evaluation used to prove the laws of the public executable evaluator.

Equations

• HexMvPolyMathlib.aevalMathlib x = (MvPolynomial.aeval x).comp ↑HexMvPolyMathlib.algEquiv

theorem HexMvPolyMathlib.aevalMathlib_apply {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (aevalMathlib x) p = (MvPolynomial.aeval x) (toMvPolynomial p)

Applying the auxiliary transported evaluator uses Mathlib evaluation after conversion.

theorem HexMvPolyMathlib.monoProd_eq_prod {n : ℕ} {S : Type v} [CommSemiring S] (x : Fin n → S) (m : Hex.Mono n) : Hex.Mono.prod x m = ∏ i : Fin n, x i ^ (monoEquiv m) i

Executable monomial evaluation is the corresponding finite product.

noncomputable def HexMvPolyMathlib.eval₂MathlibHom {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] [CommSemiring S] (f : R →+* S) (x : Fin n → S) : Hex.MvPoly n R cmp →+* S

Evaluation transported through the Mathlib equivalence.

This auxiliary homomorphism supplies the laws for the public direct evaluator.

Equations

• HexMvPolyMathlib.eval₂MathlibHom f x = (MvPolynomial.eval₂Hom f x).comp HexMvPolyMathlib.equiv.toRingHom

theorem HexMvPolyMathlib.eval₂MathlibHom_apply {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] [CommSemiring S] (f : R →+* S) (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (eval₂MathlibHom f x) p = Hex.MvPoly.eval₂ (⇑f) x p

The Mathlib-transported evaluation homomorphism applies as direct eval₂.

theorem HexMvPolyMathlib.aevalMathlib_eq_eval₂ {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (aevalMathlib x) p = Hex.MvPoly.eval₂ (⇑(algebraMap R S)) x p

The auxiliary transported algebra evaluator is exactly the Mathlib-free direct evaluator with the coefficient algebra map.

def HexMvPolyMathlib.eval₂Hom {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Fin n → S) : Hex.MvPoly n R cmp →+* S

Evaluation along an arbitrary coefficient ring homomorphism, packaged as a ring homomorphism on executable polynomials. Its function field is definitionally the direct Mathlib-free evaluator; lawful boolean equality is converted to proposition-level equality only inside the erased law proofs.

Equations

• HexMvPolyMathlib.eval₂Hom f x = { toFun := Hex.MvPoly.eval₂ (⇑f) x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexMvPolyMathlib.eval₂Hom_apply {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (eval₂Hom f x) p = Hex.MvPoly.eval₂ (⇑f) x p

The packaged ring homomorphism is the Mathlib-free direct evaluator.

def HexMvPolyMathlib.aeval {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) : Hex.MvPoly n R cmp →ₐ[R] S

Executable algebra evaluation. The function field is definitionally the direct Mathlib-free evaluator.

Equations

• HexMvPolyMathlib.aeval x = { toRingHom := HexMvPolyMathlib.eval₂Hom (algebraMap R S) x, commutes' := ⋯ }

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

Applying executable algebra evaluation agrees with Mathlib evaluation after conversion.

theorem HexMvPolyMathlib.aeval_eq_eval₂ {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (aeval x) p = Hex.MvPoly.eval₂ (⇑(algebraMap R S)) x p

Algebra-hom evaluation is exactly the Mathlib-free direct evaluator with the coefficient algebra map.

theorem HexMvPolyMathlib.aeval_eq_eval {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] (x : Fin n → R) (p : Hex.MvPoly n R cmp) : (aeval x) p = Hex.MvPoly.eval x p

Evaluation into the coefficient ring agrees with the Mathlib-free specialization.

@[simp]

theorem HexMvPolyMathlib.aeval_zero {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) : (aeval x) 0 = 0

Algebra evaluation sends zero to zero.

@[simp]

theorem HexMvPolyMathlib.aeval_one {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) : (aeval x) 1 = 1

Algebra evaluation sends one to one.

@[simp]

theorem HexMvPolyMathlib.aeval_add {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p q : Hex.MvPoly n R cmp) : (aeval x) (p + q) = (aeval x) p + (aeval x) q

Algebra evaluation preserves addition.

@[simp]

theorem HexMvPolyMathlib.aeval_mul {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p q : Hex.MvPoly n R cmp) : (aeval x) (p * q) = (aeval x) p * (aeval x) q

Algebra evaluation preserves multiplication.

@[simp]

theorem HexMvPolyMathlib.aeval_pow {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : Hex.MvPoly n R cmp) (k : ℕ) : (aeval x) (p ^ k) = (aeval x) p ^ k

Algebra evaluation preserves natural powers.

@[simp]

theorem HexMvPolyMathlib.aeval_C {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (r : R) : (aeval x) (Hex.MvPoly.C r) = (algebraMap R S) r

Algebra evaluation sends a constant polynomial through the algebra map.

@[simp]

theorem HexMvPolyMathlib.aeval_X {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (i : Fin n) : (aeval x) (Hex.MvPoly.X i) = x i

Algebra evaluation sends a variable polynomial to its assigned value.

@[simp]

theorem HexMvPolyMathlib.aeval_neg {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [CommRing S] [Algebra R S] (x : Fin n → S) (p : Hex.MvPoly n R cmp) : (aeval x) (-p) = -(aeval x) p

Algebra evaluation preserves negation.

@[simp]

theorem HexMvPolyMathlib.aeval_sub {n : ℕ} {R : Type u} {S : Type v} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [CommRing S] [Algebra R S] (x : Fin n → S) (p q : Hex.MvPoly n R cmp) : (aeval x) (p - q) = (aeval x) p - (aeval x) q

Algebra evaluation preserves subtraction.