Definition df-cytp 39810

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 39809	. 2 class CytP
2		vn	. . 3 setvar 𝑛
3		cn 11640	. . 3 class ℕ
4		ccnfld 20547	. . . . . 6 class ℂfld
5		cpl1 20347	. . . . . 6 class Poly1
6	4, 5	cfv 6357	. . . . 5 class (Poly1‘ℂfld)
7		cmgp 19241	. . . . 5 class mulGrp
8	6, 7	cfv 6357	. . . 4 class (mulGrp‘(Poly1‘ℂfld))
9		vr	. . . . 5 setvar 𝑟
10	4, 7	cfv 6357	. . . . . . . . 9 class (mulGrp‘ℂfld)
11		cc 10537	. . . . . . . . . 10 class ℂ
12		cc0 10539	. . . . . . . . . . 11 class 0
13	12	csn 4569	. . . . . . . . . 10 class {0}
14	11, 13	cdif 3935	. . . . . . . . 9 class (ℂ ∖ {0})
15		cress 16486	. . . . . . . . 9 class ↾s
16	10, 14, 15	co 7158	. . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17		cod 18654	. . . . . . . 8 class od
18	16, 17	cfv 6357	. . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
19	18	ccnv 5556	. . . . . 6 class ◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
20	2	cv 1536	. . . . . . 7 class 𝑛
21	20	csn 4569	. . . . . 6 class {𝑛}
22	19, 21	cima 5560	. . . . 5 class (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23		cv1 20346	. . . . . . 7 class var1
24	4, 23	cfv 6357	. . . . . 6 class (var1‘ℂfld)
25	9	cv 1536	. . . . . . 7 class 𝑟
26		cascl 20086	. . . . . . . 8 class algSc
27	6, 26	cfv 6357	. . . . . . 7 class (algSc‘(Poly1‘ℂfld))
28	25, 27	cfv 6357	. . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29		csg 18107	. . . . . . 7 class -g
30	6, 29	cfv 6357	. . . . . 6 class (-g‘(Poly1‘ℂfld))
31	24, 28, 30	co 7158	. . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
32	9, 22, 31	cmpt 5148	. . . 4 class (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33		cgsu 16716	. . . 4 class Σg
34	8, 32, 33	co 7158	. . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
35	2, 3, 34	cmpt 5148	. 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
36	1, 35	wceq 1537	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  39815  cytpval  39816