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 41573
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 41572 . 2 class CytP
2 vn . . 3 setvar 𝑛
3 cn 12158 . . 3 class β„•
4 ccnfld 20812 . . . . . 6 class β„‚fld
5 cpl1 21564 . . . . . 6 class Poly1
64, 5cfv 6497 . . . . 5 class (Poly1β€˜β„‚fld)
7 cmgp 19901 . . . . 5 class mulGrp
86, 7cfv 6497 . . . 4 class (mulGrpβ€˜(Poly1β€˜β„‚fld))
9 vr . . . . 5 setvar π‘Ÿ
104, 7cfv 6497 . . . . . . . . 9 class (mulGrpβ€˜β„‚fld)
11 cc 11054 . . . . . . . . . 10 class β„‚
12 cc0 11056 . . . . . . . . . . 11 class 0
1312csn 4587 . . . . . . . . . 10 class {0}
1411, 13cdif 3908 . . . . . . . . 9 class (β„‚ βˆ– {0})
15 cress 17117 . . . . . . . . 9 class β†Ύs
1610, 14, 15co 7358 . . . . . . . 8 class ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))
17 cod 19311 . . . . . . . 8 class od
1816, 17cfv 6497 . . . . . . 7 class (odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})))
1918ccnv 5633 . . . . . 6 class β—‘(odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})))
202cv 1541 . . . . . . 7 class 𝑛
2120csn 4587 . . . . . 6 class {𝑛}
2219, 21cima 5637 . . . . 5 class (β—‘(odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) β€œ {𝑛})
23 cv1 21563 . . . . . . 7 class var1
244, 23cfv 6497 . . . . . 6 class (var1β€˜β„‚fld)
259cv 1541 . . . . . . 7 class π‘Ÿ
26 cascl 21274 . . . . . . . 8 class algSc
276, 26cfv 6497 . . . . . . 7 class (algScβ€˜(Poly1β€˜β„‚fld))
2825, 27cfv 6497 . . . . . 6 class ((algScβ€˜(Poly1β€˜β„‚fld))β€˜π‘Ÿ)
29 csg 18755 . . . . . . 7 class -g
306, 29cfv 6497 . . . . . 6 class (-gβ€˜(Poly1β€˜β„‚fld))
3124, 28, 30co 7358 . . . . 5 class ((var1β€˜β„‚fld)(-gβ€˜(Poly1β€˜β„‚fld))((algScβ€˜(Poly1β€˜β„‚fld))β€˜π‘Ÿ))
329, 22, 31cmpt 5189 . . . 4 class (π‘Ÿ ∈ (β—‘(odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) β€œ {𝑛}) ↦ ((var1β€˜β„‚fld)(-gβ€˜(Poly1β€˜β„‚fld))((algScβ€˜(Poly1β€˜β„‚fld))β€˜π‘Ÿ)))
33 cgsu 17327 . . . 4 class Ξ£g
348, 32, 33co 7358 . . 3 class ((mulGrpβ€˜(Poly1β€˜β„‚fld)) Ξ£g (π‘Ÿ ∈ (β—‘(odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) β€œ {𝑛}) ↦ ((var1β€˜β„‚fld)(-gβ€˜(Poly1β€˜β„‚fld))((algScβ€˜(Poly1β€˜β„‚fld))β€˜π‘Ÿ))))
352, 3, 34cmpt 5189 . 2 class (𝑛 ∈ β„• ↦ ((mulGrpβ€˜(Poly1β€˜β„‚fld)) Ξ£g (π‘Ÿ ∈ (β—‘(odβ€˜((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) β€œ {𝑛}) ↦ ((var1β€˜β„‚fld)(-gβ€˜(Poly1β€˜β„‚fld))((algScβ€˜(Poly1β€˜β„‚fld))β€˜π‘Ÿ)))))
361, 35wceq 1542 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  41578  cytpval  41579
  Copyright terms: Public domain W3C validator