Documentation

Mathlib.RingTheory.WittVector.MulP

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.

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

    Multiplication by n is a polynomial function.