mathlib documentation


Identities between operations on the ring of Witt vectors #

In this file we derive common identities between the Frobenius and Verschiebung operators.

Main declarations #

References #

The composition of Frobenius and Verschiebung is multiplication by p.

Verschiebung is the same as multiplication by p on the ring of Witt vectors of zmod p.

theorem witt_vector.coeff_p_pow {p : } {R : Type u_1} [fact ( p)] [comm_ring R] [char_p R p] (i : ) :
(p ^ i).coeff i = 1

The “projection formula” for Frobenius and Verschiebung.