16.3. Evaluation🔗

Evaluating a polynomial p : R[X] at an element translates into one of three different definitions, depending on where the element lives:

Polynomial.eval: p.eval r when r : R;
Polynomial.eval₂: p.eval₂ f a when a : A and f : R →+* A, evaluating the polynomial in A after pushing its coefficients through f;
Polynomial.aeval: p.aeval a when A is an R-algebra and a : A.

These three are related: Polynomial.aeval_def shows that aeval is eval₂ specialised to the algebraMap, and Polynomial.eval_map rewrites eval₂ as an ordinary eval after first Polynomial.map-ping the coefficients.

16.3.1. Evaluating at a ring element🔗

For p of type R[X] and r of type R, the value of p at r is Polynomial.eval, written p.eval r:

example : R := p.eval r

16.3.2. Evaluating into an algebra🔗

When the coefficients live in a commutative semiring and we want to substitute an element of an R-algebra A for X, use Polynomial.aeval. It is the algebra homomorphism extending the algebra map (algebraMap R A : R →+* A) by sending X to a chosen element a:

aeval a : R[X] →ₐ[R] A#check (aeval a : R[X] →ₐ[R] A)

Use aeval (not eval) whenever the point of evaluation lives in a ring different from the coefficient ring, for instance, evaluating a polynomial in ℤ[X] at a real number, or at a matrix.