TY  - RPRT
TI  - Formalizing the Ring of Witt Vectors
AU  - Johan Commelin
AU  - Robert Y. Lewis
PY  - 2020
DO  - 10.1145/3437992.3439919
UR  - https://arxiv.org/abs/2010.02595
ID  - 2010.02595
ER  -