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 27522
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 27521 . 2  class CytP
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 ccnfld 16377 . . . . . 6  classfld
5 cpl1 16252 . . . . . 6  class Poly1
64, 5cfv 5255 . . . . 5  class  (Poly1 ` fld )
7 cmgp 15325 . . . . 5  class mulGrp
86, 7cfv 5255 . . . 4  class  (mulGrp `  (Poly1 ` fld ) )
9 vr . . . . 5  set  r
104, 7cfv 5255 . . . . . . . . 9  class  (mulGrp ` fld )
11 cc 8735 . . . . . . . . . 10  class  CC
12 cc0 8737 . . . . . . . . . . 11  class  0
1312csn 3640 . . . . . . . . . 10  class  { 0 }
1411, 13cdif 3149 . . . . . . . . 9  class  ( CC 
\  { 0 } )
15 cress 13149 . . . . . . . . 9  classs
1610, 14, 15co 5858 . . . . . . . 8  class  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
17 cod 14840 . . . . . . . 8  class  od
1816, 17cfv 5255 . . . . . . 7  class  ( od
`  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
1918ccnv 4688 . . . . . 6  class  `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
202cv 1622 . . . . . . 7  class  n
2120csn 3640 . . . . . 6  class  { n }
2219, 21cima 4692 . . . . 5  class  ( `' ( od `  (
(mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) " {
n } )
23 cv1 16251 . . . . . . 7  class var1
244, 23cfv 5255 . . . . . 6  class  (var1 ` fld )
259cv 1622 . . . . . . 7  class  r
26 cascl 16052 . . . . . . . 8  class algSc
276, 26cfv 5255 . . . . . . 7  class  (algSc `  (Poly1 ` fld ) )
2825, 27cfv 5255 . . . . . 6  class  ( (algSc `  (Poly1 ` fld ) ) `  r
)
29 csg 14365 . . . . . . 7  class  -g
306, 29cfv 5255 . . . . . 6  class  ( -g `  (Poly1 ` fld ) )
3124, 28, 30co 5858 . . . . 5  class  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) )
329, 22, 31cmpt 4077 . . . 4  class  ( r  e.  ( `' ( od `  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
" { n }
)  |->  ( (var1 ` fld ) ( -g `  (Poly1 ` fld )
) ( (algSc `  (Poly1 ` fld ) ) `  r
) ) )
33 cgsu 13401 . . . 4  class  gsumg
348, 32, 33co 5858 . . 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 4077 . 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 1623 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  27527  cytpval  27528
  Copyright terms: Public domain W3C validator