Multiplication by n in the ring of Witt vectors #

In this file we show that multiplication by n in the ring of Witt vectors is a polynomial function. We then use this fact to show that the composition of Frobenius and Verschiebung is equal to multiplication by p.

Main declarations #

References #

noncomputable def WittVector.wittMulN (p : ) [hp : Fact (Nat.Prime p)] :

wittMulN p n is the family of polynomials that computes the coefficients of x * n in terms of the coefficients of the Witt vector x.

Instances For
    theorem WittVector.mulN_coeff {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ) (x : WittVector p R) (k : ) :
    theorem WittVector.mulN_isPoly (p : ) [hp : Fact (Nat.Prime p)] (n : ) :
    WittVector.IsPoly p fun R _Rcr x => x * n

    Multiplication by n is a polynomial function.