no goals
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q
induction k <;>
simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ, add_mul, add_comm]