Scalar-multiple polynomial evaluation in an opposite monoid

Polynomial.smeval evaluates a polynomial at an element of an additive commutative monoid with natural number powers and an action of the coefficient semiring. All three of those structures are inherited by the opposite monoid, and MulOpposite.unop respects each of them, so evaluation commutes with MulOpposite.unop.

This is what transports a statement proved through an antihomomorphism -- a homomorphism to the opposite ring -- back to the ring itself, in the situation where only powers of a single element occur and multiplication is therefore never actually reversed. The antipode of a universal enveloping algebra applied to a generalized binomial coefficient is such a situation, since Ring.choose is a rational multiple of the value of descPochhammer at one element.

Main results

• Polynomial.unop_smeval: MulOpposite.unop commutes with Polynomial.smeval.

@[simp]

theorem Polynomial.unop_smeval {R : Type u_1} {A : Type u_2} [Semiring R] [Monoid A] [AddCommMonoid A] [Module R A] (p : Polynomial R) (a : Aᵐᵒᵖ) : MulOpposite.unop (p.smeval a) = p.smeval (MulOpposite.unop a)

Evaluating a polynomial at an element of an opposite monoid and then taking MulOpposite.unop is the same as evaluating at the MulOpposite.unop of that element.