ofSubring — Mathlib

English

Given a polynomial with coefficients in a subring T, there is a corresponding polynomial in R[X] whose coefficients are the same elements but viewed in R.

Русский

Имеется полином в R[X], полученный из полинома p с коэффициентами в T, коэффициенты которого те же элементы, но рассмотренные в R.

LaTeX

$$$\\mathrm{ofSubring}(p) = \\sum_{i \\in \\mathrm{support}(p)} \\mathrm{monomial}\\ i\\ (p.coeff i)$$$

Lean4

/-- Given a polynomial whose coefficients are in some subring, return
the corresponding polynomial whose coefficients are in the ambient ring. -/
def ofSubring (p : T[X]) : R[X] :=
  ∑ i ∈ p.support, monomial i (p.coeff i : R)

Похожие утверждения