mathlib

5dc720d1 - 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 <Rob.y.lewis@gmail.com>