p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑p)⁻¹
rw [← @Rat.cast_coe_nat ℝ _ p]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹
rw [← @Rat.cast_coe_nat ℚ_[p] _ p]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹
simp [hp.1.ne_zero, hp.1.ne_one, norm, padicNorm, padicValRat, padicValInt, zpow_neg,
  -Rat.cast_coe_nat]