Evaluation of polynomials in subrings #
Main results #
mem_map_rangeS
,mem_map_range
: the range ofmapRingHom f
consists of polynomials with coefficients in the range off
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))