Polynomial evaluation lemmas

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem Polynomial.map_iterate_eval {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (p : Polynomial R) (z : R) (j : ℕ) : f ((fun (y : R) => eval y p)^[j] z) = (fun (x : S) => eval x (map f p))^[j] (f z)

A ring homomorphism intertwines iterated evaluation of p with iterated evaluation of the mapped polynomial.

theorem Polynomial.aeval_intCast_map {L : Type u_1} {K : Type u_2} [CommRing L] [CommRing K] [Algebra L K] (p : Polynomial ℤ) (m : ℤ) : (aeval ↑m) (map (Int.castRingHom L) p) = ↑(eval m p)

Evaluating the L-reduction of an integer polynomial at an integer point of an L-algebra yields the cast of the integral value.