padic_norm): list of prime_pow_factors, valuation of prime power (#8473)

Commit

4 years ago

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

Parents

1b96e977

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

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