mathlib

3edf2b27 - feat(ring_theory/DVR,padics/padic_integers): characterize ideals of DVRs, apply to `Z_p` (#3827)

feat(ring_theory/DVR,padics/padic_integers): characterize ideals of DVRs, apply to `Z_p` (#3827) Also introduce the p-adic valuation on `Z_p`, stolen from the perfectoid project. Coauthored by: Johan Commelin <johan@commelin.net> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>