mathlib3

f1531ea5 - feat(ring_theory/witt_vector): witt_sub, a demonstration of is_poly techniques (#5165)