Definition df-cytp

Description: The Nthcyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	df-cytp	$$⊢\mathrm{CytP}=\left(n\in \mathbb{N}⟼\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccytp	$$class\mathrm{CytP}$$
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		cmgp	$$class\mathrm{mulGrp}$$
4		cpl1	$$class{\mathrm{Poly}}_1$$
5		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
6	5 4	cfv	$$class{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
7	6 3	cfv	$$class{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}$$
8		cgsu	$$class{\Sigma }_{𝑔}$$
9		vr	$$setvarr$$
10		cod	$$class\mathrm{od}$$
11	5 3	cfv	$$class{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
12		cress	$$class{\upharpoonright }_{𝑠}$$
13		cc	$$classℂ$$
14		cc0	$$class0$$
15	14	csn	$$class\left\{0\right\}$$
16	13 15	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
17	11 16 12	co	$$class\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
18	17 10	cfv	$$class\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
19	18	ccnv	$$class{\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}$$
20	1	cv	$$setvarn$$
21	20	csn	$$class\left\{n\right\}$$
22	19 21	cima	$$class{\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]$$
23		cv1	$$class{\mathrm{var}}_1$$
24	5 23	cfv	$$class{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
25		csg	$$class{-}_{𝑔}$$
26	6 25	cfv	$$class{-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}$$
27		cascl	$$class\mathrm{algSc}$$
28	6 27	cfv	$$class\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)$$
29	9	cv	$$setvarr$$
30	29 28	cfv	$$class\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)$$
31	24 30 26	co	$$class\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)$$
32	9 22 31	cmpt	$$class\left(r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]⟼{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)$$
33	7 32 8	co	$$class\left(\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}},\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$
34	1 2 33	cmpt	$$class\left(n\in \mathbb{N}⟼\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$
35	0 34	wceq	$$wff\mathrm{CytP}=\left(n\in \mathbb{N}⟼\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$