feat(data/padics): more valuations, facts about norms (#3790)
Assorted lemmas about the `p`-adics. @jcommelin and I are adding algebraic structure here as part of the Witt vector development.
Some of these declarations are stolen shamelessly 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>
