Definition df-cytp 43626

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 43625	. 2 class CytP
2		vn	. . 3 setvar 𝑛
3		cn 12174	. . 3 class ℕ
4		ccnfld 21352	. . . . . 6 class ℂfld
5		cpl1 22140	. . . . . 6 class Poly1
6	4, 5	cfv 6498	. . . . 5 class (Poly1‘ℂfld)
7		cmgp 20121	. . . . 5 class mulGrp
8	6, 7	cfv 6498	. . . 4 class (mulGrp‘(Poly1‘ℂfld))
9		vr	. . . . 5 setvar 𝑟
10	4, 7	cfv 6498	. . . . . . . . 9 class (mulGrp‘ℂfld)
11		cc 11036	. . . . . . . . . 10 class ℂ
12		cc0 11038	. . . . . . . . . . 11 class 0
13	12	csn 4567	. . . . . . . . . 10 class {0}
14	11, 13	cdif 3886	. . . . . . . . 9 class (ℂ ∖ {0})
15		cress 17200	. . . . . . . . 9 class ↾s
16	10, 14, 15	co 7367	. . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17		cod 19499	. . . . . . . 8 class od
18	16, 17	cfv 6498	. . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
19	18	ccnv 5630	. . . . . 6 class ◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
20	2	cv 1541	. . . . . . 7 class 𝑛
21	20	csn 4567	. . . . . 6 class {𝑛}
22	19, 21	cima 5634	. . . . 5 class (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23		cv1 22139	. . . . . . 7 class var1
24	4, 23	cfv 6498	. . . . . 6 class (var1‘ℂfld)
25	9	cv 1541	. . . . . . 7 class 𝑟
26		cascl 21832	. . . . . . . 8 class algSc
27	6, 26	cfv 6498	. . . . . . 7 class (algSc‘(Poly1‘ℂfld))
28	25, 27	cfv 6498	. . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29		csg 18911	. . . . . . 7 class -g
30	6, 29	cfv 6498	. . . . . 6 class (-g‘(Poly1‘ℂfld))
31	24, 28, 30	co 7367	. . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
32	9, 22, 31	cmpt 5166	. . . 4 class (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33		cgsu 17403	. . . 4 class Σg
34	8, 32, 33	co 7367	. . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
35	2, 3, 34	cmpt 5166	. 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
36	1, 35	wceq 1542	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  43629  cytpval  43630