mathlib

e7c2bba1 - feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838)

feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838) Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>