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 : RingHom R S) {p : Polynomial S} : Iff (Membership.mem (mapRingHom f).rangeS p) (∀ (n : Nat), Membership.mem f.rangeS (p.coeff n))

theorem Polynomial.mem_map_range {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : RingHom R S) {p : Polynomial S} : Iff (Membership.mem (mapRingHom f).range p) (∀ (n : Nat), Membership.mem f.range (p.coeff n))