Hi!
The `R gsum F` operation is a repeated group operation, but from a ring
`R`, one can get the multiplicative group `M = (mulGrp ` R )`.
Then `M gsum F` becomes a repeated multiplicative operation, which is
what you need here (the product of a list of factors).
There is also a `( .g ` R )` group multiple function, which is a
repeated group operation (every term is the same). When used on the
multiplicative group, it is the exponentiation you need.
As a side note, in the case of a the decomposition of a polynomial,
maybe you could use a single function, without powers:
\begin{equation*}
g=\prod_{i\in \mathrm{dom} s}(x- s(i))
\end{equation*}
Then all roots are simple when `s` is injective.
This might make things easier.
BR,
_
Thierry
On 10/04/2025 00:55, 'Meta Kunt' via Metamath wrote:
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
<https://www.eclipso.eu>*.
--
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 [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/3c80deb45e287639d48927a3bde99078%40mail.eclipso.de
<https://groups.google.com/d/msgid/metamath/3c80deb45e287639d48927a3bde99078%40mail.eclipso.de?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/88760f70-b8f5-4c67-ac9f-3bd7e9d7d3f2%40gmx.net.
