Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cytp Unicode version

Definition df-cytp 27625
Description: The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Assertion
Ref Expression
df-cytp  |- CytP  =  ( n  e.  NN  |->  ( (mulGrp `  (Poly1 ` fld ) )  gsumg  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) ) ) )
Distinct variable group:    n, r

Detailed syntax breakdown of Definition df-cytp
StepHypRef Expression
1 ccytp 27624 . 2  class CytP
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 ccnfld 16393 . . . . . 6  classfld
5 cpl1 16268 . . . . . 6  class Poly1
64, 5cfv 5271 . . . . 5  class  (Poly1 ` fld )
7 cmgp 15341 . . . . 5  class mulGrp
86, 7cfv 5271 . . . 4  class  (mulGrp `  (Poly1 ` fld ) )
9 vr . . . . 5  set  r
104, 7cfv 5271 . . . . . . . . 9  class  (mulGrp ` fld )
11 cc 8751 . . . . . . . . . 10  class  CC
12 cc0 8753 . . . . . . . . . . 11  class  0
1312csn 3653 . . . . . . . . . 10  class  { 0 }
1411, 13cdif 3162 . . . . . . . . 9  class  ( CC 
\  { 0 } )
15 cress 13165 . . . . . . . . 9  classs
1610, 14, 15co 5874 . . . . . . . 8  class  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
17 cod 14856 . . . . . . . 8  class  od
1816, 17cfv 5271 . . . . . . 7  class  ( od
`  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
1918ccnv 4704 . . . . . 6  class  `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
202cv 1631 . . . . . . 7  class  n
2120csn 3653 . . . . . 6  class  { n }
2219, 21cima 4708 . . . . 5  class  ( `' ( od `  (
(mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )
23 cv1 16267 . . . . . . 7  class var1
244, 23cfv 5271 . . . . . 6  class  (var1 ` fld )
259cv 1631 . . . . . . 7  class  r
26 cascl 16068 . . . . . . . 8  class algSc
276, 26cfv 5271 . . . . . . 7  class  (algSc `  (Poly1 ` fld ) )
2825, 27cfv 5271 . . . . . 6  class  ( (algSc `  (Poly1 ` fld ) ) `  r
)
29 csg 14381 . . . . . . 7  class  -g
306, 29cfv 5271 . . . . . 6  class  ( -g `  (Poly1 ` fld ) )
3124, 28, 30co 5874 . . . . 5  class  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) )
329, 22, 31cmpt 4093 . . . 4  class  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
" { n }
)  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) )
33 cgsu 13417 . . . 4  class  gsumg
348, 32, 33co 5874 . . 3  class  ( (mulGrp `  (Poly1 ` fld ) )  gsumg  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) ) )
352, 3, 34cmpt 4093 . 2  class  ( n  e.  NN  |->  ( (mulGrp `  (Poly1 ` fld ) )  gsumg  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) ) ) )
361, 35wceq 1632 1  wff CytP  =  ( n  e.  NN  |->  ( (mulGrp `  (Poly1 ` fld ) )  gsumg  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  cytpfn  27630  cytpval  27631
  Copyright terms: Public domain W3C validator