p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
rw [norm_def]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)
exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _