English
For a polynomial p ∈ R[X], the restricted polynomial lies in Polynomial (Subring.closure (coeffs p)) and is the formal sum of monomials with coefficients in that closure.
Русский
Для многочлена p ∈ R[X] ограниченный по кольцу полином записывается как сумма мономов с коэффициентами в замыкании подкольца.
LaTeX
$$restriction(p) = \sum_{i ∈ supp(p)} \ monomial i (⟨p_coeff i, proof⟩ : Subring.closure (↑p.coeffs))$$
Lean4
/-- Given a polynomial, return the polynomial whose coefficients are in
the ring closure of the original coefficients. -/
def restriction (p : R[X]) : Polynomial (Subring.closure (↑p.coeffs : Set R)) :=
∑ i ∈ p.support,
monomial i
(⟨p.coeff i,
letI := Classical.decEq R
if H : p.coeff i = 0 then H.symm ▸ (Subring.closure _).zero_mem
else Subring.subset_closure (p.coeff_mem_coeffs H)⟩ :
Subring.closure (↑p.coeffs : Set R))
