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.

src/algebra/gcd_monoid/nat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 import algebra.gcd_monoid.finset
-import number_theory.padics.padic_norm
+import number_theory.padics.padic_val
 
 /-!
 # Basic results about setwise gcds on ℕ

src/group_theory/exponent.lean

@@ -7,7 +7,7 @@ import group_theory.order_of_element
 import algebra.punit_instances
 import algebra.gcd_monoid.finset
 import tactic.by_contra
-import number_theory.padics.padic_norm
+import number_theory.padics.padic_val
 
 /-!
 # Exponent of a group