Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(NumberTheory/Padics/PadicVal): Add `padicValNat_mul_pow_left/rig…
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
- Loading branch information