p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ↑(padicNorm p ↑k) ≤ ↑(↑p ^ (-↑n)) ↔ ↑(p ^ n) ∣ k
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ↑(padicNorm p ↑k) ≤ ↑(↑p ^ (-↑n)) ↔ ↑(p ^ n) ∣ k
norm_cast
no goals
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
rw [← padicNorm.dvd_iff_norm_le]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
simp
no goals
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ↑k = ↑↑k
norm_cast