mathlib3

435b97ac - feat(ring_theory/witt_vector): the comparison between W(F_p) and Z_p (#5164)

feat(ring_theory/witt_vector): the comparison between W(F_p) and Z_p (#5164) This PR is the culmination of the Witt vector project. We prove that the ring of Witt vectors over `zmod p` is isomorphic to the ring of `p`-adic numbers. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>