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 38566
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 38565 . 2 class CytP
2 vn . . 3 setvar 𝑛
3 cn 11312 . . 3 class
4 ccnfld 20068 . . . . . 6 class fld
5 cpl1 19869 . . . . . 6 class Poly1
64, 5cfv 6101 . . . . 5 class (Poly1‘ℂfld)
7 cmgp 18805 . . . . 5 class mulGrp
86, 7cfv 6101 . . . 4 class (mulGrp‘(Poly1‘ℂfld))
9 vr . . . . 5 setvar 𝑟
104, 7cfv 6101 . . . . . . . . 9 class (mulGrp‘ℂfld)
11 cc 10222 . . . . . . . . . 10 class
12 cc0 10224 . . . . . . . . . . 11 class 0
1312csn 4368 . . . . . . . . . 10 class {0}
1411, 13cdif 3766 . . . . . . . . 9 class (ℂ ∖ {0})
15 cress 16185 . . . . . . . . 9 class s
1610, 14, 15co 6878 . . . . . . . 8 class ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
17 cod 18257 . . . . . . . 8 class od
1816, 17cfv 6101 . . . . . . 7 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
1918ccnv 5311 . . . . . 6 class (od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
202cv 1652 . . . . . . 7 class 𝑛
2120csn 4368 . . . . . 6 class {𝑛}
2219, 21cima 5315 . . . . 5 class ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛})
23 cv1 19868 . . . . . . 7 class var1
244, 23cfv 6101 . . . . . 6 class (var1‘ℂfld)
259cv 1652 . . . . . . 7 class 𝑟
26 cascl 19634 . . . . . . . 8 class algSc
276, 26cfv 6101 . . . . . . 7 class (algSc‘(Poly1‘ℂfld))
2825, 27cfv 6101 . . . . . 6 class ((algSc‘(Poly1‘ℂfld))‘𝑟)
29 csg 17740 . . . . . . 7 class -g
306, 29cfv 6101 . . . . . 6 class (-g‘(Poly1‘ℂfld))
3124, 28, 30co 6878 . . . . 5 class ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))
329, 22, 31cmpt 4922 . . . 4 class (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))
33 cgsu 16416 . . . 4 class Σg
348, 32, 33co 6878 . . 3 class ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))
352, 3, 34cmpt 4922 . 2 class (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ ((od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
361, 35wceq 1653 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  38571  cytpval  38572
  Copyright terms: Public domain W3C validator