Metamath Proof Explorer


Theorem cytpfn

Description: Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Assertion cytpfn CytP Fn

Proof

Step Hyp Ref Expression
1 ovex mulGrp Poly 1 fld r od mulGrp fld 𝑠 0 -1 n var 1 fld - Poly 1 fld algSc Poly 1 fld r V
2 df-cytp CytP = n mulGrp Poly 1 fld r od mulGrp fld 𝑠 0 -1 n var 1 fld - Poly 1 fld algSc Poly 1 fld r
3 1 2 fnmpti CytP Fn