Commit 2024-04-05 19:57 62cf98c3
View on Github →feat(NumberTheory/Padics/PadicVal): Add padicValNat_mul_pow_left/right (#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