Batch Evaluation Correctness

Correctness theorems for univariate batch-evaluation implementations.

theorem CompPoly.CPolynomial.evalBatchHorner_eq_evalBatch {R : Type u_1} [Semiring R] (p : CPolynomial R) (xs : Array R) : p.evalBatchHorner xs = p.evalBatch xs

Batched Horner evaluation agrees with the direct batched evaluator.

theorem CompPoly.CPolynomial.evalBatchSubproduct_eq_evalBatch {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (D : ModContext R) (p : CPolynomial R) (xs : Array R) : evalBatchSubproduct M D p xs = p.evalBatch xs

Subproduct-tree batch evaluation agrees with the direct batched evaluator.