p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ↑(↑padicNormE ↑q) = ↑(padicNorm p q)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ‖↑q‖ = ↑(padicNorm p q)
dsimp [norm]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ↑(↑padicNormE ↑q) = ↑(padicNorm p q)
rw [← padicNormE.eq_padic_norm']