feat(data/nat/prime, number_theory/padics/padic_norm): list of prime_pow_factors, valuation of prime power (#8473)

Co-authored-by: ineswright <52750254+ineswright@users.noreply.github.com>

Author: ineswright

src/data/nat/prime.lean

@@ -664,6 +664,16 @@ have hn : 0 < n := nat.pos_of_ne_zero $ λ h, begin
 end,
 perm_of_prod_eq_prod (by rwa prod_factors hn) h₂ (@prime_of_mem_factors _)
 
+lemma prime.factors_pow {p : ℕ} (hp : p.prime) (n : ℕ) :
+  (p ^ n).factors = list.repeat p n :=
+begin
+  symmetry,
+  rw ← list.repeat_perm,
+  apply nat.factors_unique (list.prod_repeat p n),
+  { intros q hq,
+    rwa eq_of_mem_repeat hq },
+end
+
 end
 
 lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : prime p) {m n k l : ℕ}

src/number_theory/padics/padic_norm.lean

@@ -373,6 +373,15 @@ begin
     exact_mod_cast split_frac, }
 end
 
+/-- A version of `padic_val_rat.pow` for `padic_val_nat` -/
+protected lemma pow (p q n : ℕ) [fact p.prime] (hq : q ≠ 0) :
+  padic_val_nat p (q ^ n) = n * padic_val_nat p q :=
+begin
+  apply @nat.cast_injective ℤ,
+  push_cast,
+  exact padic_val_rat.pow _ (cast_ne_zero.mpr hq),
+end
+
 end padic_val_nat
 
 section padic_val_nat
@@ -469,6 +478,12 @@ begin
     rwa nat.coprime_primes hp.1 hq.1, },
 end
 
+@[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
+by simp [padic_val_nat_def (fact.out p.prime).ne_zero]
+
+@[simp] lemma padic_val_nat_prime_pow (p n : ℕ) [fact p.prime] : padic_val_nat p (p ^ n) = n :=
+by rw [padic_val_nat.pow p _ _ (fact.out p.prime).ne_zero, padic_val_nat_self p, mul_one]
+
 open_locale big_operators
 
 lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :