Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-12 09:52 e245b24b

View on Github →

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

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.prime.factors_pow

Modified src/number_theory/padics/padic_norm.lean

added theorem padic_val_nat_prime_pow

added theorem padic_val_nat_self