The value of the image of a polynomial at a rational point #
A candidate for Mathlib.Algebra.Polynomial.Eval.Coeff, next to Polynomial.eval_natCast_map and
Polynomial.eval_intCast_map: under a map of division rings, the image of a polynomial takes at a
rational number the image of the value of the polynomial there (Polynomial.eval_ratCast_map).
Main statements #
Polynomial.eval_ratCast_map: the value of the image of a polynomial at a rational number.
@[simp]
theorem
Polynomial.eval_ratCast_map
{R : Type u_1}
{S : Type u_2}
[DivisionRing R]
[DivisionRing S]
(f : R →+* S)
(p : Polynomial R)
(q : ℚ)
: