Commit 2020-07-20 06:04 5080dd56

feat(data/padics/padic_norm): lemmas about padic_val_nat (#3230) Collection of lemmas about padic_val_nat, culminating in lemma prod_pow_prime_padic_val_nat : ∀ (n : nat) (s : n ≠ 0) (m : nat) (pr : n < m), ∏ p in finset.filter nat.prime (finset.range m), pow p (padic_val_nat p n) = n.