Hi!
I've been playing with a proof[0] about the sum of roots of a simple
polynomial and wanted to use `vieta1`. I landed on the following
representation:
( ph -> sum_ y e. ( `' ( z e. CC |-> sum_ k e. ( 0 ... 2 ) ( ( <" -u 6
3 9 "> ` k ) x. ( z ^ k ) ) ) " { 0 } ) y = -u ( 3 / 9 ) )
and demonstrated its equality to the original polynomial:
```
( z e. CC |-> ( ( ( 9 x. ( z ^ 2 ) ) + ( 3 x. z ) ) - 6 ) )
```
But deep in the weeds of the proof I realize that the use of a `Word`
is quite unfortunate, as `vieta1` (through `coeff`) and `dgrval`
expect the coefficients to be defined over NN0 and not a finite
sequence.
I was curious to hear from folks what is the preferred/recommended way
to represent a particular polynomial to use with these theorems?
Thanks thanks and hope you have a wonderful break!
-stan
[0] AMC 12 2000 p15
```
|- ( ph -> F : CC --> CC )
|- ( ph -> A. x e. CC ( F ` ( x / 3 ) ) = ( ( ( x ^ 2 ) + x ) + 1 ) )
|- ( ph -> sum_ y e. ( `' F " { 7 } ) ( y / 3 ) = -u ( 1 / 9 ) )
```
--
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 on the web visit
https://groups.google.com/d/msgid/metamath/CACZd_0y%3DEABQKkaQJNoVvNeyR%3D9yHxcBkF7jVA4UuJZz6WE-PA%40mail.gmail.com.
