Polynomial evaluation signs under ordered embeddings

Mapping coefficients and the evaluation point through a strictly monotone ring homomorphism preserves the sign of the value. This applies to embeddings into ordered real closures.

theorem Polynomial.sign_eval_map {R : Type u_1} {S : Type u_2} [Semiring R] [LinearOrder R] [Semiring S] [Preorder S] [DecidableLT S] (p : Polynomial R) (f : R →+* S) (hf : StrictMono ⇑f) (x : R) : SignType.sign (eval (f x) (map f p)) = SignType.sign (eval x p)

Mapping a polynomial and its evaluation point through a strictly monotone ring homomorphism preserves its sign.