chore(number_theory/padics/padic_norm): golf `prod_pow_prime_padic_val_nat` (#12034)
chore(number_theory/padics/padic_norm): golf `prod_pow_prime_padic_val_nat` (#12034)

A todo comment said "this proof can probably be golfed with `factorization` stuff"; it turns out that indeed it can be. :)



Co-authored-by: Rob Lewis <f89db59e6074667375662ee222555a187f42739f@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib