Evaluation of polynomials in subrings

Main results

• mem_map_rangeS, mem_map_range: the range of mapRingHom f consists of polynomials with coefficients in the range of f

theorem Polynomial.mem_map_rangeS {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial S} : p ∈ (Polynomial.mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

theorem Polynomial.mem_map_range {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {p : Polynomial S} : p ∈ (Polynomial.mapRingHom f).range ↔ ∀ (n : ℕ), p.coeff n ∈ f.range