Users' Mathboxes 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 38098
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 38097 . 2 class CytP
2 vn . . 3 setvar 𝑛
3 cn 11058 . . 3 class
4 ccnfld 19794 . . . . . 6 class fld
5 cpl1 19595 . . . . . 6 class Poly1
64, 5cfv 5926 . . . . 5 class (Poly1‘ℂfld)
7 cmgp 18535 . . . . 5 class mulGrp
86, 7cfv 5926 . . . 4 class (mulGrp‘(Poly1‘ℂfld))
9 vr . . . . 5 setvar 𝑟
104, 7cfv 5926 . . . . . . . . 9 class (mulGrp‘ℂfld)
11 cc 9972 . . . . . . . . . 10 class
12 cc0 9974 . . . . . . . . . . 11 class 0
1312csn 4210 . . . . . . . . . 10 class {0}
1411, 13cdif 3604 . . . . . . . . 9 class (ℂ ∖ {0})
15 cress 15905 . . . . . . . . 9 class s
1610, 14, 15co 6690 . . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17 cod 17990 . . . . . . . 8 class od
1816, 17cfv 5926 . . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
1918ccnv 5142 . . . . . 6 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
202cv 1522 . . . . . . 7 class 𝑛
2120csn 4210 . . . . . 6 class {𝑛}
2219, 21cima 5146 . . . . 5 class ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23 cv1 19594 . . . . . . 7 class var1
244, 23cfv 5926 . . . . . 6 class (var1‘ℂfld)
259cv 1522 . . . . . . 7 class 𝑟
26 cascl 19359 . . . . . . . 8 class algSc
276, 26cfv 5926 . . . . . . 7 class (algSc‘(Poly1‘ℂfld))
2825, 27cfv 5926 . . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29 csg 17471 . . . . . . 7 class -g
306, 29cfv 5926 . . . . . 6 class (-g‘(Poly1‘ℂfld))
3124, 28, 30co 6690 . . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
329, 22, 31cmpt 4762 . . . 4 class (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33 cgsu 16148 . . . 4 class Σg
348, 32, 33co 6690 . . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
352, 3, 34cmpt 4762 . 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
361, 35wceq 1523 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  38103  cytpval  38104
  Copyright terms: Public domain W3C validator