Commit 2022-04-26 20:19 b00a7f8a

refactor(number_theory/padics/padic_norm): split file (#13576) This PR splits the initial part of the padic_norm.lean file that defines p-adic valuations into a new file called padic_val.lean. This split makes sense to me since it seems most files importing this don't actually use the norm, so those files can build more in parallel. It also seems like a good organizational change: This way people can look at the files in this directory and see immediately where the valuation is defined, and people looking for the definition of padic_norm in padic_norm.lean don't have to scroll.