mathlib3

8a4b491c - feat(ring_theory/witt_vector/structure_polynomial): {map_}witt_structure_int (#4465)

feat(ring_theory/witt_vector/structure_polynomial): {map_}witt_structure_int (#4465) This is the second PR in a series on a fundamental theorem about Witt polynomials. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>