Definition df-cytp 36800

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 36799	. 2 class CytP
2		vn	. . 3 setvar 𝑛
3		cn 10897	. . 3 class ℕ
4		ccnfld 19567	. . . . . 6 class ℂfld
5		cpl1 19368	. . . . . 6 class Poly1
6	4, 5	cfv 5804	. . . . 5 class (Poly1‘ℂfld)
7		cmgp 18312	. . . . 5 class mulGrp
8	6, 7	cfv 5804	. . . 4 class (mulGrp‘(Poly1‘ℂfld))
9		vr	. . . . 5 setvar 𝑟
10	4, 7	cfv 5804	. . . . . . . . 9 class (mulGrp‘ℂfld)
11		cc 9813	. . . . . . . . . 10 class ℂ
12		cc0 9815	. . . . . . . . . . 11 class 0
13	12	csn 4125	. . . . . . . . . 10 class {0}
14	11, 13	cdif 3537	. . . . . . . . 9 class (ℂ ∖ {0})
15		cress 15696	. . . . . . . . 9 class ↾s
16	10, 14, 15	co 6549	. . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17		cod 17767	. . . . . . . 8 class od
18	16, 17	cfv 5804	. . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
19	18	ccnv 5037	. . . . . 6 class ◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
20	2	cv 1474	. . . . . . 7 class 𝑛
21	20	csn 4125	. . . . . 6 class {𝑛}
22	19, 21	cima 5041	. . . . 5 class (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23		cv1 19367	. . . . . . 7 class var1
24	4, 23	cfv 5804	. . . . . 6 class (var1‘ℂfld)
25	9	cv 1474	. . . . . . 7 class 𝑟
26		cascl 19132	. . . . . . . 8 class algSc
27	6, 26	cfv 5804	. . . . . . 7 class (algSc‘(Poly1‘ℂfld))
28	25, 27	cfv 5804	. . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29		csg 17247	. . . . . . 7 class -g
30	6, 29	cfv 5804	. . . . . 6 class (-g‘(Poly1‘ℂfld))
31	24, 28, 30	co 6549	. . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
32	9, 22, 31	cmpt 4643	. . . 4 class (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33		cgsu 15924	. . . 4 class Σg
34	8, 32, 33	co 6549	. . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
35	2, 3, 34	cmpt 4643	. 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
36	1, 35	wceq 1475	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  36805  cytpval  36806