English
If a polynomial with coefficients in R has all its coefficients in a subring T, there is a canonical polynomial in T[X] representing the same polynomial.
Русский
Если все коэффициенты полинома из R лежат в подкольце T, существует канонический полином в T[X], представляющий тот же полином.
LaTeX
$$$\\text{toSubring}(p, T, hp) \\in T[X] \\quad \\text{has the same coefficients as } p$$$
Lean4
/-- Given a polynomial `p` and a subring `T` that contains the coefficients of `p`,
return the corresponding polynomial whose coefficients are in `T`. -/
def toSubring (hp : (↑p.coeffs : Set R) ⊆ T) : T[X] :=
∑ i ∈ p.support,
monomial i
(⟨p.coeff i,
letI := Classical.decEq R
if H : p.coeff i = 0 then H.symm ▸ T.zero_mem else hp (p.coeff_mem_coeffs H)⟩ :
T)
