English
An element p ∈ S[X] lies in the range of mapRingHom f if and only if all coefficients of p lie in the range of f.
Русский
Элемент p∈S[X] принадлежит образу mapRingHom f тогда и только тогда, когда все коэффициенты p лежат в образе f.
LaTeX
$$$p \\in (\\mathrm{mapRingHom}\ f).\\mathrm{rangeS} \\iff \\forall n, p.\\mathrm{coeff}(n) \\in f.\\mathrm{rangeS}$$$
Lean4
theorem mem_map_rangeS {p : S[X]} : p ∈ (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]
