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 ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

theorem Polynomial.notMem_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

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

theorem Polynomial.notMem_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