English
Given a polynomial P over K with coefficients in the subring R, there is a corresponding polynomial in R[X] with the same coefficients.
Русский
Дано полином P над K, коэффициенты которого лежат в подкольце R; существует соответствующий полином в R[X] с такими же коэффициентами.
LaTeX
$$$\forall P\in K[X],\bigl(\forall n, P_{coeff}(n)\in R\bigr)\Rightarrow \exists Q\in R[X],\forall n, Q_{coeff}(n)=P_{coeff}(n)$$$
Lean4
/-- Given a polynomial in `K[X]` such that all coefficients belong to the subring `R`,
`Polynomial.int` is the corresponding polynomial in `R[X]`. -/
def int (P : K[X]) (hP : ∀ n : ℕ, P.coeff n ∈ R) : R[X] where
toFinsupp :=
{ support := P.support
toFun := fun n => ⟨P.coeff n, hP n⟩
mem_support_toFun := fun n => by rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff] }
