Evaluation at a central scalar

For an R-algebra S, possibly noncommutative, the element algebraMap R S t is central, so evaluating polynomials with coefficients in S at it is a ring homomorphism S[X] →+* S. Over a noncommutative ring evaluation at an arbitrary point is not multiplicative, so Mathlib's Polynomial.evalRingHom is only available over commutative rings.

The value at algebraMap R S t expands as a sum of the coefficients of p weighted by the powers of t.

def Polynomial.evalAlgebraMapRingHom {R : Type u_1} (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (t : R) : Polynomial S →+* S

Evaluation at the central element algebraMap R S t, as a ring homomorphism.

@[simp]

theorem Polynomial.evalAlgebraMapRingHom_apply {R : Type u_1} (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (t : R) (p : Polynomial S) : (evalAlgebraMapRingHom S t) p = eval ((algebraMap R S) t) p

theorem Polynomial.eval_algebraMap_eq_sum_range {R : Type u_1} (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (p : Polynomial S) (t : R) : eval ((algebraMap R S) t) p = ∑ i ∈ Finset.range (p.natDegree + 1), t ^ i • p.coeff i

Evaluating a polynomial at the image of a scalar t combines its coefficients with the powers of t.