Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cytp Structured version   Visualization version   GIF version

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
StepHypRef 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
64, 5cfv 5804 . . . . 5 class (Poly1‘ℂfld)
7 cmgp 18312 . . . . 5 class mulGrp
86, 7cfv 5804 . . . 4 class (mulGrp‘(Poly1‘ℂfld))
9 vr . . . . 5 setvar 𝑟
104, 7cfv 5804 . . . . . . . . 9 class (mulGrp‘ℂfld)
11 cc 9813 . . . . . . . . . 10 class
12 cc0 9815 . . . . . . . . . . 11 class 0
1312csn 4125 . . . . . . . . . 10 class {0}
1411, 13cdif 3537 . . . . . . . . 9 class (ℂ ∖ {0})
15 cress 15696 . . . . . . . . 9 class s
1610, 14, 15co 6549 . . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17 cod 17767 . . . . . . . 8 class od
1816, 17cfv 5804 . . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
1918ccnv 5037 . . . . . 6 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
202cv 1474 . . . . . . 7 class 𝑛
2120csn 4125 . . . . . 6 class {𝑛}
2219, 21cima 5041 . . . . 5 class ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23 cv1 19367 . . . . . . 7 class var1
244, 23cfv 5804 . . . . . 6 class (var1‘ℂfld)
259cv 1474 . . . . . . 7 class 𝑟
26 cascl 19132 . . . . . . . 8 class algSc
276, 26cfv 5804 . . . . . . 7 class (algSc‘(Poly1‘ℂfld))
2825, 27cfv 5804 . . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29 csg 17247 . . . . . . 7 class -g
306, 29cfv 5804 . . . . . 6 class (-g‘(Poly1‘ℂfld))
3124, 28, 30co 6549 . . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
329, 22, 31cmpt 4643 . . . 4 class (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33 cgsu 15924 . . . 4 class Σg
348, 32, 33co 6549 . . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
352, 3, 34cmpt 4643 . 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
361, 35wceq 1475 1 wff CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
 Colors of variables: wff setvar class This definition is referenced by:  cytpfn  36805  cytpval  36806
 Copyright terms: Public domain W3C validator