New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/witt_vector): Witt vectors are a DVR #12213
Conversation
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Can you also update the description? |
I've updated the PR description, renamed the file, and done a little reogranizing! |
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
All of the private calculational lemmas were really just used for one theorem. I moved them to all be together, renamed them to |
LGTM. I think everything above it resolved, but I'll delegate rather than merge so an author can make the final call. bors d+ |
✌️ robertylewis can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
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>
Pull request successfully merged into master. Build succeeded: |
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 indiscrete_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
Branched from #12041