Commit 2020-10-30 11:09 d28e3d10

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