feat(data/padics/padic_norm) Fix namespacing of padic_val_nat (#3207)

No longer need we `padic_val_rat.padic_val_nat`.

src/data/padics/padic_norm.lean

@@ -76,7 +76,6 @@ dif_pos ⟨hq, hp.ne_one⟩
 
 namespace padic_val_rat
 open multiplicity
-section padic_val_rat
 variables {p : ℕ}
 
 /--
@@ -114,14 +113,14 @@ by rw [padic_val_rat, dif_pos]; simp *; refl
 
 end padic_val_rat
 
-section padic_val_nat
-
 /--
 A convenience function for the case of `padic_val_rat` when both inputs are natural numbers.
 -/
 def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
 int.to_nat (padic_val_rat p n)
 
+section padic_val_nat
+
 /--
 `padic_val_nat` is defined as an `int.to_nat` cast; this lemma ensures that the cast is well-behaved.
 -/
@@ -161,7 +160,7 @@ end
 
 end padic_val_nat
 
-section padic_val_rat
+namespace padic_val_rat
 open multiplicity
 variables (p : ℕ) [p_prime : fact p.prime]
 include p_prime
@@ -298,7 +297,6 @@ theorem min_le_padic_val_rat_add {q r : ℚ}
     (by rwa add_comm) h)
 
 end padic_val_rat
-end padic_val_rat
 
 /--
 If `q ≠ 0`, the p-adic norm of a rational `q` is `p ^ (-(padic_val_rat p q))`.