[Metamath] Definition of product of polynomials.

['Meta Kunt' via Metamath]

­Given following data:
R (commutative ring with 1)
F: ( ZZ i^i Fin) --> NN0 (Maps from subset of integers to nonnegative integers.
I'd like to define the following two polynomials in R[X].
Given the canonical embedding from ZZ to R, which is denoted by s and a F with above domain and codomain,
\begin{equation*}
g=\prod_{i\in \mathrm{dom} F}(x- s(i))^{F(i))
\end{equation*}
This should be a polynomial in R[X].
I'd also like to define for r in R and a positive integers e the following two polynomials.
g(x^e) and g(x)^e, both as polynomials of R[X]
g is the product of finitely many monomials (x-s(a))
h1 =g(x^e)
h2= g(x)^e

I can't see how I can define the polynomials at the easiest.

The closest I can find is this https://us.metamath.org/mpeuni/lply1binomsc.html
But I need the product of polynomials and not the sum.

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/3c80deb45e287639d48927a3bde99078%40mail.eclipso.de.