Module docstring
{"# Evaluation of polynomials in subrings
Main results
mem_map_rangeS,mem_map_range: the range ofmapRingHom fconsists of polynomials with coefficients in the range off
"}
Polynomial.mem_map_rangeS
theorem
{p : S[X]} : p ∈ (mapRingHom f).rangeS ↔ ∀ n, p.coeff n ∈ f.rangeS
Full source
theorem mem_map_rangeS {p : S[X]} : p ∈ (mapRingHom f).rangeSp ∈ (mapRingHom f).rangeS ↔ ∀ n, p.coeff n ∈ f.rangeS := by
constructor
· rintro ⟨p, rfl⟩ n
rw [coe_mapRingHom, coeff_map]
exact Set.mem_range_self _
· intro h
rw [p.as_sum_range_C_mul_X_pow]
refine (mapRingHom f).rangeS.sum_mem ?_
intro i _hi
rcases h i with ⟨c, hc⟩
use C c * X ^ i
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]Informal description
Let $R$ and $S$ be semirings and $f : R \to S$ be a ring homomorphism. A polynomial $p \in S[X]$ belongs to the range of the induced polynomial ring homomorphism $\text{mapRingHom}(f) : R[X] \to S[X]$ if and only if every coefficient of $p$ belongs to the range of $f$.
Polynomial.mem_map_range
theorem
{R S : Type*} [Ring R] [Ring S] (f : R →+* S) {p : S[X]} : p ∈ (mapRingHom f).range ↔ ∀ n, p.coeff n ∈ f.range
Full source
theorem mem_map_range {R S : Type*} [Ring R] [Ring S] (f : R →+* S) {p : S[X]} :
p ∈ (mapRingHom f).rangep ∈ (mapRingHom f).range ↔ ∀ n, p.coeff n ∈ f.range :=
mem_map_rangeS fInformal description
Let $R$ and $S$ be rings and $f : R \to S$ be a ring homomorphism. A polynomial $p \in S[X]$ belongs to the range of the induced polynomial ring homomorphism $\text{mapRingHom}(f) : R[X] \to S[X]$ if and only if every coefficient of $p$ belongs to the range of $f$.