mathlib3

04b55727 - feat(ring_theory/witt_vector/defs): type of witt vectors + ring operations (#4332)