feat(ring_theory/witt_vector): Witt vectors are a DVR (#12213)
This PR adds two connected files. `mul_coeff.lean` adds an auxiliary result that's used in a few places in #12041 . One of these places is in `discrete_valuation_ring.lean`, which shows that Witt vectors over a perfect field form a DVR.
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
