Definition df-cytp 37781

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

Step	Hyp	Ref	Expression
1		ccytp 37780	. 2 class CytP
2		vn	. . 3 setvar n
3		cn 11020	. . 3 class NN
4		ccnfld 19746	. . . . . 6 class ℂfld
5		cpl1 19547	. . . . . 6 class Poly1
6	4, 5	cfv 5888	. . . . 5 class (Poly1 ` ℂfld )
7		cmgp 18489	. . . . 5 class mulGrp
8	6, 7	cfv 5888	. . . 4 class (mulGrp ` (Poly1 ` ℂfld ) )
9		vr	. . . . 5 setvar r
10	4, 7	cfv 5888	. . . . . . . . 9 class (mulGrp ` ℂfld )
11		cc 9934	. . . . . . . . . 10 class CC
12		cc0 9936	. . . . . . . . . . 11 class 0
13	12	csn 4177	. . . . . . . . . 10 class { 0 }
14	11, 13	cdif 3571	. . . . . . . . 9 class ( CC \ { 0 } )
15		cress 15858	. . . . . . . . 9 class ↾s
16	10, 14, 15	co 6650	. . . . . . . 8 class ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )
17		cod 17944	. . . . . . . 8 class od
18	16, 17	cfv 5888	. . . . . . 7 class ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) )
19	18	ccnv 5113	. . . . . 6 class `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) )
20	2	cv 1482	. . . . . . 7 class n
21	20	csn 4177	. . . . . 6 class { n }
22	19, 21	cima 5117	. . . . 5 class ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } )
23		cv1 19546	. . . . . . 7 class var1
24	4, 23	cfv 5888	. . . . . 6 class (var1 ` ℂfld )
25	9	cv 1482	. . . . . . 7 class r
26		cascl 19311	. . . . . . . 8 class algSc
27	6, 26	cfv 5888	. . . . . . 7 class (algSc ` (Poly1 ` ℂfld ) )
28	25, 27	cfv 5888	. . . . . 6 class ( (algSc ` (Poly1 ` ℂfld ) ) ` r )
29		csg 17424	. . . . . . 7 class -g
30	6, 29	cfv 5888	. . . . . 6 class ( -g ` (Poly1 ` ℂfld ) )
31	24, 28, 30	co 6650	. . . . 5 class ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) )
32	9, 22, 31	cmpt 4729	. . . 4 class ( r e. ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } ) |-> ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) ) )
33		cgsu 16101	. . . 4 class gsumg
34	8, 32, 33	co 6650	. . 3 class ( (mulGrp ` (Poly1 ` ℂfld ) ) gsumg ( r e. ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } ) |-> ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) ) ) )
35	2, 3, 34	cmpt 4729	. 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 ) ) ) ) )
36	1, 35	wceq 1483	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 ) ) ) ) )

This definition is referenced by:  cytpfn  37786  cytpval  37787