Definition df-cytp 40731

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 = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))

Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-cytp

Step	Hyp	Ref	Expression
1		ccytp 40730	. 2 class CytP
2		vn	. . 3 setvar 𝑛
3		cn 11830	. . 3 class ℕ
4		ccnfld 20363	. . . . . 6 class ℂfld
5		cpl1 21098	. . . . . 6 class Poly1
6	4, 5	cfv 6380	. . . . 5 class (Poly1‘ℂfld)
7		cmgp 19504	. . . . 5 class mulGrp
8	6, 7	cfv 6380	. . . 4 class (mulGrp‘(Poly1‘ℂfld))
9		vr	. . . . 5 setvar 𝑟
10	4, 7	cfv 6380	. . . . . . . . 9 class (mulGrp‘ℂfld)
11		cc 10727	. . . . . . . . . 10 class ℂ
12		cc0 10729	. . . . . . . . . . 11 class 0
13	12	csn 4541	. . . . . . . . . 10 class {0}
14	11, 13	cdif 3863	. . . . . . . . 9 class (ℂ ∖ {0})
15		cress 16784	. . . . . . . . 9 class ↾s
16	10, 14, 15	co 7213	. . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17		cod 18916	. . . . . . . 8 class od
18	16, 17	cfv 6380	. . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
19	18	ccnv 5550	. . . . . 6 class ◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
20	2	cv 1542	. . . . . . 7 class 𝑛
21	20	csn 4541	. . . . . 6 class {𝑛}
22	19, 21	cima 5554	. . . . 5 class (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23		cv1 21097	. . . . . . 7 class var1
24	4, 23	cfv 6380	. . . . . 6 class (var1‘ℂfld)
25	9	cv 1542	. . . . . . 7 class 𝑟
26		cascl 20814	. . . . . . . 8 class algSc
27	6, 26	cfv 6380	. . . . . . 7 class (algSc‘(Poly1‘ℂfld))
28	25, 27	cfv 6380	. . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29		csg 18367	. . . . . . 7 class -g
30	6, 29	cfv 6380	. . . . . 6 class (-g‘(Poly1‘ℂfld))
31	24, 28, 30	co 7213	. . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
32	9, 22, 31	cmpt 5135	. . . 4 class (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33		cgsu 16945	. . . 4 class Σg
34	8, 32, 33	co 7213	. . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
35	2, 3, 34	cmpt 5135	. 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
36	1, 35	wceq 1543	1 wff CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))

This definition is referenced by:  cytpfn  40736  cytpval  40737