mathlib

d28e3d10 - feat(ring_theory/witt_vector/is_poly): supporting ghost calculations (#4691)

feat(ring_theory/witt_vector/is_poly): supporting ghost calculations (#4691) Most operations on Witt vectors can be described/defined by evaluating integral polynomials on the coefficients of Witt vectors. One can prove identities between combinations of such operations by applying the non-injective ghost map, and continuing to prove the resulting identity of ghost components. Such a calculation is called a ghost calculation. This file provides the theoretical justification for why applying the non-injective ghost map is a legal move, and it provides tactics that aid in applying this step to the point that it is almost transparent. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>