First PR: Witt vectors mod p

Stream: mathlib4

[Saul Glasman]

Hi all, I've lurked here before but I am now opening my (very modest) first PR, implementing a TODO in the theory of Witt vectors. Looking forward to feedback!

https://github.com/leanprover-community/mathlib4/pull/33310

[Joël Riou]

Nice! I have added some suggestions.

[Johan Commelin]

@Saul Glasman Thanks for the PR! Note that you can simply write #33310 in your message, and Zulip will render it as #33310.