mathlib3

90026aee - feat(ring_theory/witt_vector): assorted facts about Witt vectors over char p rings