Description: Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cytpfn | |- CytP Fn NN |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovex | |- ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) e. _V |
|
| 2 | df-cytp | |- CytP = ( n e. NN |-> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) ) |
|
| 3 | 1 2 | fnmpti | |- CytP Fn NN |