# mathlib3documentation

ring_theory.witt_vector.mul_p

## Multiplication by n in the ring of Witt vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• mul_n_is_poly: multiplication by n is a polynomial function

## References #

noncomputable def witt_vector.witt_mul_n (p : ) [hp : fact (nat.prime p)] :

witt_mul_n 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
• (n + 1) = λ (k : ),
theorem witt_vector.mul_n_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ) (x : R) (k : ) :
(x * n).coeff k = k)
@[instance]
def witt_vector.mul_n_is_poly.comp₂_i (p : ) [hp : fact (nat.prime p)] (n : ) (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : (x y : R), (λ (R : Type u_1) (_Rcr : (x : R), x * n) R _Rcr (f x y))
theorem witt_vector.mul_n_is_poly (p : ) [hp : fact (nat.prime p)] (n : ) :
(λ (R : Type u_1) (_Rcr : (x : R), x * n)

Multiplication by n is a polynomial function.

@[instance]
def witt_vector.mul_n_is_poly.comp_i (p : ) [hp : fact (nat.prime p)] (n : ) (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : , (λ (R : Type u_1) (_Rcr : (x : R), x * n) R _Rcr f)
@[simp]
theorem witt_vector.bind₁_witt_mul_n_witt_polynomial (p : ) [hp : fact (nat.prime p)] (n k : ) :
k) = n * k