# 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`

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