mathlib3

d768e46f - feat(ring_theory/witt_vector/structure_polynomial): witt_structure_rat{_prop} (#4464)

feat(ring_theory/witt_vector/structure_polynomial): witt_structure_rat{_prop} (#4464) This is the first PR in a series on a fundamental theorem for Witt polynomials. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>