Evaluation of computable multivariate polynomials, bundled and over Finsets

CompPoly records that CMvPolynomial.eval vals respects each ring operation separately (eval_zero, eval_one, eval_add, eval_mul, eval_C, …), which is what simp/grind need to normalize a fixed expression. Two things are missing for reasoning about a family of polynomials: the value of a bare variable, and commutation with Finset.sum / Finset.prod.

Both follow at once from bundling: CMvPolynomial.eval vals is eval₂Hom (RingHom.id R) vals, so map_sum and map_prod apply verbatim. evalHom records that bundling; the two Finset lemmas are its immediate corollaries, stated in unbundled form so that call sites can rewrite without unfolding.

def CPoly.CMvPolynomial.evalHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) : CMvPolynomial n R →+* R

Evaluation at a fixed point, bundled as a ring homomorphism — the identity-coefficient case of eval₂Hom. This is what gives evaluation the map_* API of a RingHom.

@[simp]

theorem CPoly.CMvPolynomial.evalHom_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p : CMvPolynomial n R) : (evalHom vals) p = eval vals p

@[simp]

theorem CPoly.CMvPolynomial.eval_zero {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) : eval vals 0 = 0

@[simp]

theorem CPoly.CMvPolynomial.eval_one {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) : eval vals 1 = 1

@[simp]

theorem CPoly.CMvPolynomial.eval_C {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (c : R) : eval vals (C c) = c

@[simp]

theorem CPoly.CMvPolynomial.eval_X {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (i : Fin n) : eval vals (X i) = vals i

@[simp]

theorem CPoly.CMvPolynomial.eval_add {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p q : CMvPolynomial n R) : eval vals (p + q) = eval vals p + eval vals q

@[simp]

theorem CPoly.CMvPolynomial.eval_mul {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p q : CMvPolynomial n R) : eval vals (p * q) = eval vals p * eval vals q

@[simp]

theorem CPoly.CMvPolynomial.eval_pow {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p : CMvPolynomial n R) (k : ℕ) : eval vals (p ^ k) = eval vals p ^ k

@[simp]

theorem CPoly.CMvPolynomial.eval_neg {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p : CMvPolynomial n R) : eval vals (-p) = -eval vals p

@[simp]

theorem CPoly.CMvPolynomial.eval_sub {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] (vals : Fin n → R) (p q : CMvPolynomial n R) : eval vals (p - q) = eval vals p - eval vals q

theorem CPoly.CMvPolynomial.eval_sum {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) {ι : Type u_2} (s : Finset ι) (f : ι → CMvPolynomial n R) : eval vals (∑ i ∈ s, f i) = ∑ i ∈ s, eval vals (f i)

Evaluation commutes with a finite sum of polynomials.

theorem CPoly.CMvPolynomial.eval_prod {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (vals : Fin n → R) {ι : Type u_2} (s : Finset ι) (f : ι → CMvPolynomial n R) : eval vals (∏ i ∈ s, f i) = ∏ i ∈ s, eval vals (f i)

Evaluation commutes with a finite product of polynomials.

Transporting a whole polynomial

The lemmas above are enough for statements about values. A statement about degrees is not determined by values (two distinct polynomials agree everywhere over a finite field), so it has to cross the representation boundary at the level of the polynomial itself, through fromCMvPolynomial. That map is the forward direction of polyRingEquiv, hence a ring homomorphism, so it too commutes with Finset.sum and Finset.prod.

theorem CPoly.CMvPolynomial.eval_ext_univariate {R : Type u_2} [CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [IsDomain R] {p q : CMvPolynomial 1 R} {d : ℕ} {S : Finset R} (hdeg : MvPolynomial.degreeOf 0 (fromCMvPolynomial p - fromCMvPolynomial q) ≤ d) (hagree : d < {r ∈ S | eval (fun (x : Fin 1) => r) p = eval (fun (x : Fin 1) => r) q}.card) : p = q

Bridge from univariate eval-extensionality. Two single-variable CMvPolynomials over an integral domain that agree on more than $d$ points of a Finset S are equal, when $d$ bounds the degreeOf 0 of their difference through the CPolynomial.cmvEquiv bridge.

The hypothesis form matches Schwartz–Zippel usage at call sites: callers typically have a degree bound on the difference polynomial, not on p and q individually.